-- File: subLibrary -- This files gives two proofs of lemma Eq_sub__Eq_super in Section 8.3.1. Path "../lol" Path "../lolplus" Load "lambdaLsubplus" Load "logic" -- No implicit arguments now! Prove Eq_sub__Eq_super : @B:*s. @A<:B. @x,y:A. (=) A x y -> (=) B x y -- The command -- Deduction Eq_sub__Eq_super -- gives: -- --------------- -- 1 | B : *s | hyp -- 2 | A <: B : *s | hyp -- 3 | x : A | hyp -- 4 | y : A | hyp -- 5 | (=) A x y | hyp -- |-------------- -- | ------------- -- 6 | | P : B->*p | hyp -- | |------------ -- | | -------------------------- -- 7 | | | Q := \z:A. P z : A->*p | def -- | | |------------------------- -- 8 | | | @P:A->*p. P x -> P y conv 5 -- 9 | | | Q x -> Q y @E 8 -- 10 | | | P x -> P y conv 9 -- 11 | | P x -> P y defI 7-10 -- 12 | @P:B->*p. P x -> P y @I 6-11 -- 13 | (=) B x y conv 12 -- 14 @B:*s. @A <: B : *s. @x,y:A. (=) A x y -> (=) B x y @I 1-13 -- A less instructive proof is the following. Prove Eq_sub__Eq_super2 : @B:*s. @A<:B. @x,y:A. (=) A x y -> (=) B x y -- The command -- Deduction Eq_sub__Eq_super2 -- gives: -- --------------- -- 1 | B : *s | hyp -- 2 | A <: B : *s | hyp -- 3 | x : A | hyp -- 4 | y : A | hyp -- 5 | (=) A x y | hyp -- |-------------- -- 6 | (=) B x y subsum 5 -- 7 @B:*s. @A <: B : *s. @x,y:A. (=) A x y -> (=) B x y @I 1-6