John Tang Boyland - 2013-11-13

Sometimes its more powerful if we don't use the LF context for a relation or a theorem. For example, the POPLmark 1a challenge requires:

lemma narrowing :
    @Assumes(Gamma)
    forall s1: Gamma, X<:T’, Gamma’ |- T1[X] <: T2[X]
    forall s2: Gamma |- T <: T’
    exists Gamma, X<:T, Gamma’ |- T1[X] <: T2[X].
    proof by ... //
end lemma

This capability requires an LF extension described in a working paper by Boyland and Zhao.