```-- File: subLibrary

-- This files gives two proofs of lemma Eq_sub__Eq_super in Section 8.3.1.

Path "../lol"
Path "../lolplus"

-- 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

```