DEFINITION pr3_gen_cabbr()
TYPE =
∀c:C
.∀t1:T
.∀t2:T
.pr3 c t1 t2
→∀e:C
.∀u:T
.∀d:nat
.getl d c (CHead e (Bind Abbr) u)
→∀a0:C
.csubst1 d u c a0
→∀a:C
.drop (S O) d a0 a
→∀x1:T.(subst1 d u t1 (lift (S O) d x1))→(ex2 T λx2:T.subst1 d u t2 (lift (S O) d x2) λx2:T.pr3 a x1 x2)
BODY =
assume c: C
assume t1: T
assume t2: T
suppose H: pr3 c t1 t2
we proceed by induction on H to prove
∀e:C
.∀u:T
.∀d:nat
.getl d c (CHead e (Bind Abbr) u)
→∀a0:C
.csubst1 d u c a0
→∀a:C
.drop (S O) d a0 a
→∀x1:T.(subst1 d u t1 (lift (S O) d x1))→(ex2 T λx2:T.subst1 d u t2 (lift (S O) d x2) λx2:T.pr3 a x1 x2)
case pr3_refl : t:T ⇒
the thesis becomes
∀e:C
.∀u:T
.∀d:nat
.getl d c (CHead e (Bind Abbr) u)
→∀a0:C
.csubst1 d u c a0
→∀a:C
.drop (S O) d a0 a
→∀x1:T.∀H3:(subst1 d u t (lift (S O) d x1)).(ex2 T λx2:T.subst1 d u t (lift (S O) d x2) λx2:T.pr3 a x1 x2)
assume e: C
assume u: T
assume d: nat
suppose : getl d c (CHead e (Bind Abbr) u)
assume a0: C
suppose : csubst1 d u c a0
assume a: C
suppose : drop (S O) d a0 a
assume x1: T
suppose H3: subst1 d u t (lift (S O) d x1)
by (pr3_refl . .)
we proved pr3 a x1 x1
by (ex_intro2 . . . . H3 previous)
we proved ex2 T λx2:T.subst1 d u t (lift (S O) d x2) λx2:T.pr3 a x1 x2
∀e:C
.∀u:T
.∀d:nat
.getl d c (CHead e (Bind Abbr) u)
→∀a0:C
.csubst1 d u c a0
→∀a:C
.drop (S O) d a0 a
→∀x1:T.∀H3:(subst1 d u t (lift (S O) d x1)).(ex2 T λx2:T.subst1 d u t (lift (S O) d x2) λx2:T.pr3 a x1 x2)
case pr3_sing : t0:T t3:T H0:pr2 c t3 t0 t4:T :pr3 c t0 t4 ⇒
the thesis becomes
∀e:C
.∀u:T
.∀d:nat
.∀H3:getl d c (CHead e (Bind Abbr) u)
.∀a0:C
.∀H4:csubst1 d u c a0
.∀a:C
.∀H5:drop (S O) d a0 a
.∀x1:T.∀H6:(subst1 d u t3 (lift (S O) d x1)).(ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2)
(H2) by induction hypothesis we know
∀e:C
.∀u:T
.∀d:nat
.getl d c (CHead e (Bind Abbr) u)
→∀a0:C
.csubst1 d u c a0
→∀a:C
.drop (S O) d a0 a
→∀x1:T.(subst1 d u t0 (lift (S O) d x1))→(ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2)
assume e: C
assume u: T
assume d: nat
suppose H3: getl d c (CHead e (Bind Abbr) u)
assume a0: C
suppose H4: csubst1 d u c a0
assume a: C
suppose H5: drop (S O) d a0 a
assume x1: T
suppose H6: subst1 d u t3 (lift (S O) d x1)
by (pr2_gen_cabbr . . . H0 . . . H3 . H4 . H5 . H6)
we proved ex2 T λx2:T.subst1 d u t0 (lift (S O) d x2) λx2:T.pr2 a x1 x2
we proceed by induction on the previous result to prove ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2
case ex_intro2 : x:T H7:subst1 d u t0 (lift (S O) d x) H8:pr2 a x1 x ⇒
the thesis becomes ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2
by (H2 . . . H3 . H4 . H5 . H7)
we proved ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x x2
we proceed by induction on the previous result to prove ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2
case ex_intro2 : x0:T H9:subst1 d u t4 (lift (S O) d x0) H10:pr3 a x x0 ⇒
the thesis becomes ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2
by (pr3_sing . . . H8 . H10)
we proved pr3 a x1 x0
by (ex_intro2 . . . . H9 previous)
ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2
ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2
we proved ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2
∀e:C
.∀u:T
.∀d:nat
.∀H3:getl d c (CHead e (Bind Abbr) u)
.∀a0:C
.∀H4:csubst1 d u c a0
.∀a:C
.∀H5:drop (S O) d a0 a
.∀x1:T.∀H6:(subst1 d u t3 (lift (S O) d x1)).(ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2)
we proved
∀e:C
.∀u:T
.∀d:nat
.getl d c (CHead e (Bind Abbr) u)
→∀a0:C
.csubst1 d u c a0
→∀a:C
.drop (S O) d a0 a
→∀x1:T.(subst1 d u t1 (lift (S O) d x1))→(ex2 T λx2:T.subst1 d u t2 (lift (S O) d x2) λx2:T.pr3 a x1 x2)
we proved
∀c:C
.∀t1:T
.∀t2:T
.pr3 c t1 t2
→∀e:C
.∀u:T
.∀d:nat
.getl d c (CHead e (Bind Abbr) u)
→∀a0:C
.csubst1 d u c a0
→∀a:C
.drop (S O) d a0 a
→∀x1:T.(subst1 d u t1 (lift (S O) d x1))→(ex2 T λx2:T.subst1 d u t2 (lift (S O) d x2) λx2:T.pr3 a x1 x2)