(* This file was automatically generated: do not edit *********************)
-include "Basic-1/pc3/left.ma".
+include "basic_1/pc3/left.ma".
-include "Basic-1/fsubst0/defs.ma".
+include "basic_1/fsubst0/fwd.ma".
-include "Basic-1/csubst0/getl.ma".
+include "basic_1/csubst0/getl.ma".
-theorem pc3_pr2_fsubst0:
+lemma pc3_pr2_fsubst0:
\forall (c1: C).(\forall (t1: T).(\forall (t: T).((pr2 c1 t1 t) \to (\forall
(i: nat).(\forall (u: T).(\forall (c2: C).(\forall (t2: T).((fsubst0 i u c1
t1 c2 t2) \to (\forall (e: C).((getl i c1 (CHead e (Bind Abbr) u)) \to (pc3
(x3: T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
x2))).(\lambda (H10: (getl i c0 (CHead x1 (Bind x0) x3))).(\lambda (H11:
(subst0 (minus i0 (S i)) u0 x2 x3)).(let H12 \def (f_equal C C (\lambda (e0:
-C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
-(CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
-x2) H9) in ((let H13 \def (f_equal C B (\lambda (e0: C).(match e0 in C return
-(\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
-\Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
-x1 (Bind x0) x2) H9) in ((let H14 \def (f_equal C T (\lambda (e0: C).(match
-e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _
-t5) \Rightarrow t5])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H9) in
-(\lambda (H15: (eq B Abbr x0)).(\lambda (H16: (eq C d x1)).(let H17 \def
-(eq_ind_r T x2 (\lambda (t5: T).(subst0 (minus i0 (S i)) u0 t5 x3)) H11 u
-H14) in (let H18 \def (eq_ind_r C x1 (\lambda (c3: C).(getl i c0 (CHead c3
-(Bind x0) x3))) H10 d H16) in (let H19 \def (eq_ind_r B x0 (\lambda (b:
-B).(getl i c0 (CHead d (Bind b) x3))) H18 Abbr H15) in (ex2_ind T (\lambda
-(t5: T).(subst0 i x3 t3 t5)) (\lambda (t5: T).(subst0 (S (plus (minus i0 (S
-i)) i)) u0 t0 t5)) (pc3 c0 t2 t0) (\lambda (x: T).(\lambda (H20: (subst0 i x3
-t3 x)).(\lambda (H21: (subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x)).(let
-H22 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i)) (\lambda (n:
-nat).(subst0 n u0 t0 x)) H21 i0 (lt_plus_minus_r i i0 H6)) in (pc3_pr2_u c0 x
-t2 (pr2_delta c0 d x3 i H19 t2 t3 H1 x H20) t0 (pc3_pr2_x c0 x t0 (pr2_delta
-c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H4 (CHead e (Bind Abbr)
-u0) H5) t0 t0 (pr0_refl t0) x H22))))))) (subst0_subst0_back t3 t0 u i H2 x3
-u0 (minus i0 (S i)) H17)))))))) H13)) H12))))))))) H8)) (\lambda (H8: (ex3_4
-B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq
-C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b:
-B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c0 (CHead e2
+C).(match e0 with [(CSort _) \Rightarrow d | (CHead c3 _ _) \Rightarrow c3]))
+(CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H9) in ((let H13 \def
+(f_equal C B (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow Abbr |
+(CHead _ k _) \Rightarrow (match k with [(Bind b) \Rightarrow b | (Flat _)
+\Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H9) in
+((let H14 \def (f_equal C T (\lambda (e0: C).(match e0 with [(CSort _)
+\Rightarrow u | (CHead _ _ t5) \Rightarrow t5])) (CHead d (Bind Abbr) u)
+(CHead x1 (Bind x0) x2) H9) in (\lambda (H15: (eq B Abbr x0)).(\lambda (H16:
+(eq C d x1)).(let H17 \def (eq_ind_r T x2 (\lambda (t5: T).(subst0 (minus i0
+(S i)) u0 t5 x3)) H11 u H14) in (let H18 \def (eq_ind_r C x1 (\lambda (c3:
+C).(getl i c0 (CHead c3 (Bind x0) x3))) H10 d H16) in (let H19 \def (eq_ind_r
+B x0 (\lambda (b: B).(getl i c0 (CHead d (Bind b) x3))) H18 Abbr H15) in
+(ex2_ind T (\lambda (t5: T).(subst0 i x3 t3 t5)) (\lambda (t5: T).(subst0 (S
+(plus (minus i0 (S i)) i)) u0 t0 t5)) (pc3 c0 t2 t0) (\lambda (x: T).(\lambda
+(H20: (subst0 i x3 t3 x)).(\lambda (H21: (subst0 (S (plus (minus i0 (S i))
+i)) u0 t0 x)).(let H22 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i))
+(\lambda (n: nat).(subst0 n u0 t0 x)) H21 i0 (lt_plus_minus_r i i0 H6)) in
+(pc3_pr2_u c0 x t2 (pr2_delta c0 d x3 i H19 t2 t3 H1 x H20) t0 (pc3_pr2_x c0
+x t0 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H4 (CHead
+e (Bind Abbr) u0) H5) t0 t0 (pr0_refl t0) x H22))))))) (subst0_subst0_back t3
+t0 u i H2 x3 u0 (minus i0 (S i)) H17)))))))) H13)) H12))))))))) H8)) (\lambda
+(H8: (ex3_4 B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda
+(u1: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda
+(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c0 (CHead e2
(Bind b) u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda
(_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))).(ex3_4_ind B C C T (\lambda
(b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind
(x2: C).(\lambda (x3: T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead
x1 (Bind x0) x3))).(\lambda (H10: (getl i c0 (CHead x2 (Bind x0)
x3))).(\lambda (H11: (csubst0 (minus i0 (S i)) u0 x1 x2)).(let H12 \def
-(f_equal C C (\lambda (e0: C).(match e0 in C return (\lambda (_: C).C) with
-[(CSort _) \Rightarrow d | (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind
-Abbr) u) (CHead x1 (Bind x0) x3) H9) in ((let H13 \def (f_equal C B (\lambda
-(e0: C).(match e0 in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow
-Abbr | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with
-[(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr)
-u) (CHead x1 (Bind x0) x3) H9) in ((let H14 \def (f_equal C T (\lambda (e0:
-C).(match e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
-(CHead _ _ t5) \Rightarrow t5])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
-x3) H9) in (\lambda (H15: (eq B Abbr x0)).(\lambda (H16: (eq C d x1)).(let
-H17 \def (eq_ind_r T x3 (\lambda (t5: T).(getl i c0 (CHead x2 (Bind x0) t5)))
-H10 u H14) in (let H18 \def (eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus
-i0 (S i)) u0 c3 x2)) H11 d H16) in (let H19 \def (eq_ind_r B x0 (\lambda (b:
-B).(getl i c0 (CHead x2 (Bind b) u))) H17 Abbr H15) in (pc3_pr2_r c0 t2 t0
-(pr2_delta c0 x2 u i H19 t2 t3 H1 t0 H2)))))))) H13)) H12))))))))) H8))
-(\lambda (H8: (ex4_5 B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1
-(Bind b) u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda
-(_: T).(\lambda (w: T).(getl i c0 (CHead e2 (Bind b) w))))))) (\lambda (_:
-B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
-(minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1
-e2)))))))).(ex4_5_ind B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1
-(Bind b) u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda
-(_: T).(\lambda (w: T).(getl i c0 (CHead e2 (Bind b) w))))))) (\lambda (_:
-B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
-(minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))
-(pc3 c0 t2 t0) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: C).(\lambda
-(x3: T).(\lambda (x4: T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead
-x1 (Bind x0) x3))).(\lambda (H10: (getl i c0 (CHead x2 (Bind x0)
-x4))).(\lambda (H11: (subst0 (minus i0 (S i)) u0 x3 x4)).(\lambda (H12:
-(csubst0 (minus i0 (S i)) u0 x1 x2)).(let H13 \def (f_equal C C (\lambda (e0:
-C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
+(f_equal C C (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow d |
(CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
-x3) H9) in ((let H14 \def (f_equal C B (\lambda (e0: C).(match e0 in C return
-(\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
-\Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
-x1 (Bind x0) x3) H9) in ((let H15 \def (f_equal C T (\lambda (e0: C).(match
-e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _
-t5) \Rightarrow t5])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in
+x3) H9) in ((let H13 \def (f_equal C B (\lambda (e0: C).(match e0 with
+[(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow (match k with [(Bind
+b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u)
+(CHead x1 (Bind x0) x3) H9) in ((let H14 \def (f_equal C T (\lambda (e0:
+C).(match e0 with [(CSort _) \Rightarrow u | (CHead _ _ t5) \Rightarrow t5]))
+(CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in (\lambda (H15: (eq B
+Abbr x0)).(\lambda (H16: (eq C d x1)).(let H17 \def (eq_ind_r T x3 (\lambda
+(t5: T).(getl i c0 (CHead x2 (Bind x0) t5))) H10 u H14) in (let H18 \def
+(eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus i0 (S i)) u0 c3 x2)) H11 d
+H16) in (let H19 \def (eq_ind_r B x0 (\lambda (b: B).(getl i c0 (CHead x2
+(Bind b) u))) H17 Abbr H15) in (pc3_pr2_r c0 t2 t0 (pr2_delta c0 x2 u i H19
+t2 t3 H1 t0 H2)))))))) H13)) H12))))))))) H8)) (\lambda (H8: (ex4_5 B C C T T
+(\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
+(_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1))))))) (\lambda
+(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl
+i c0 (CHead e2 (Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1 w))))))
+(\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 (minus i0 (S i)) u0 e1 e2)))))))).(ex4_5_ind B C C T T
+(\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
+(_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1))))))) (\lambda
+(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl
+i c0 (CHead e2 (Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1 w))))))
+(\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 (minus i0 (S i)) u0 e1 e2)))))) (pc3 c0 t2 t0) (\lambda (x0:
+B).(\lambda (x1: C).(\lambda (x2: C).(\lambda (x3: T).(\lambda (x4:
+T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
+x3))).(\lambda (H10: (getl i c0 (CHead x2 (Bind x0) x4))).(\lambda (H11:
+(subst0 (minus i0 (S i)) u0 x3 x4)).(\lambda (H12: (csubst0 (minus i0 (S i))
+u0 x1 x2)).(let H13 \def (f_equal C C (\lambda (e0: C).(match e0 with [(CSort
+_) \Rightarrow d | (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u)
+(CHead x1 (Bind x0) x3) H9) in ((let H14 \def (f_equal C B (\lambda (e0:
+C).(match e0 with [(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow
+(match k with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead
+d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in ((let H15 \def (f_equal C T
+(\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow u | (CHead _ _ t5)
+\Rightarrow t5])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in
(\lambda (H16: (eq B Abbr x0)).(\lambda (H17: (eq C d x1)).(let H18 \def
(eq_ind_r T x3 (\lambda (t5: T).(subst0 (minus i0 (S i)) u0 t5 x4)) H11 u
H15) in (let H19 \def (eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus i0 (S
T).(\lambda (x3: T).(\lambda (H10: (eq C (CHead d (Bind Abbr) u) (CHead x1
(Bind x0) x2))).(\lambda (H11: (getl i c0 (CHead x1 (Bind x0) x3))).(\lambda
(H12: (subst0 (minus i0 (S i)) u0 x2 x3)).(let H13 \def (f_equal C C (\lambda
-(e0: C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow
-d | (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind
-x0) x2) H10) in ((let H14 \def (f_equal C B (\lambda (e0: C).(match e0 in C
-return (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
-\Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
-x1 (Bind x0) x2) H10) in ((let H15 \def (f_equal C T (\lambda (e0: C).(match
-e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _
-t6) \Rightarrow t6])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H10) in
-(\lambda (H16: (eq B Abbr x0)).(\lambda (H17: (eq C d x1)).(let H18 \def
-(eq_ind_r T x2 (\lambda (t6: T).(subst0 (minus i0 (S i)) u0 t6 x3)) H12 u
-H15) in (let H19 \def (eq_ind_r C x1 (\lambda (c3: C).(getl i c0 (CHead c3
-(Bind x0) x3))) H11 d H17) in (let H20 \def (eq_ind_r B x0 (\lambda (b:
-B).(getl i c0 (CHead d (Bind b) x3))) H19 Abbr H16) in (ex2_ind T (\lambda
-(t6: T).(subst0 i x3 t3 t6)) (\lambda (t6: T).(subst0 (S (plus (minus i0 (S
-i)) i)) u0 t0 t6)) (pc3 c0 t5 t0) (\lambda (x: T).(\lambda (H21: (subst0 i x3
-t3 x)).(\lambda (H22: (subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x)).(let
-H23 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i)) (\lambda (n:
-nat).(subst0 n u0 t0 x)) H22 i0 (lt_plus_minus_r i i0 H7)) in (pc3_pr2_u2 c0
-t2 t5 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5
-(CHead e (Bind Abbr) u0) H6) t2 t2 (pr0_refl t2) t5 H4) t0 (pc3_pr2_u c0 x t2
-(pr2_delta c0 d x3 i H20 t2 t3 H1 x H21) t0 (pc3_pr2_x c0 x t0 (pr2_delta c0
-e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead e (Bind Abbr) u0)
-H6) t0 t0 (pr0_refl t0) x H23)))))))) (subst0_subst0_back t3 t0 u i H2 x3 u0
-(minus i0 (S i)) H18)))))))) H14)) H13))))))))) H9)) (\lambda (H9: (ex3_4 B C
-C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C
+(e0: C).(match e0 with [(CSort _) \Rightarrow d | (CHead c3 _ _) \Rightarrow
+c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H10) in ((let H14 \def
+(f_equal C B (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow Abbr |
+(CHead _ k _) \Rightarrow (match k with [(Bind b) \Rightarrow b | (Flat _)
+\Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H10) in
+((let H15 \def (f_equal C T (\lambda (e0: C).(match e0 with [(CSort _)
+\Rightarrow u | (CHead _ _ t6) \Rightarrow t6])) (CHead d (Bind Abbr) u)
+(CHead x1 (Bind x0) x2) H10) in (\lambda (H16: (eq B Abbr x0)).(\lambda (H17:
+(eq C d x1)).(let H18 \def (eq_ind_r T x2 (\lambda (t6: T).(subst0 (minus i0
+(S i)) u0 t6 x3)) H12 u H15) in (let H19 \def (eq_ind_r C x1 (\lambda (c3:
+C).(getl i c0 (CHead c3 (Bind x0) x3))) H11 d H17) in (let H20 \def (eq_ind_r
+B x0 (\lambda (b: B).(getl i c0 (CHead d (Bind b) x3))) H19 Abbr H16) in
+(ex2_ind T (\lambda (t6: T).(subst0 i x3 t3 t6)) (\lambda (t6: T).(subst0 (S
+(plus (minus i0 (S i)) i)) u0 t0 t6)) (pc3 c0 t5 t0) (\lambda (x: T).(\lambda
+(H21: (subst0 i x3 t3 x)).(\lambda (H22: (subst0 (S (plus (minus i0 (S i))
+i)) u0 t0 x)).(let H23 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i))
+(\lambda (n: nat).(subst0 n u0 t0 x)) H22 i0 (lt_plus_minus_r i i0 H7)) in
+(pc3_pr2_u2 c0 t2 t5 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c
+c0 u0 H5 (CHead e (Bind Abbr) u0) H6) t2 t2 (pr0_refl t2) t5 H4) t0
+(pc3_pr2_u c0 x t2 (pr2_delta c0 d x3 i H20 t2 t3 H1 x H21) t0 (pc3_pr2_x c0
+x t0 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead
+e (Bind Abbr) u0) H6) t0 t0 (pr0_refl t0) x H23)))))))) (subst0_subst0_back
+t3 t0 u i H2 x3 u0 (minus i0 (S i)) H18)))))))) H14)) H13))))))))) H9))
+(\lambda (H9: (ex3_4 B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u1: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1))))))
+(\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c0
+(CHead e2 (Bind b) u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))).(ex3_4_ind B C C
+T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C
(CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: B).(\lambda
(_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c0 (CHead e2 (Bind b)
u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
-T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))).(ex3_4_ind B C C T (\lambda (b:
-B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind
-Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: B).(\lambda (_: C).(\lambda
-(e2: C).(\lambda (u1: T).(getl i c0 (CHead e2 (Bind b) u1)))))) (\lambda (_:
-B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus i0 (S
-i)) u0 e1 e2))))) (pc3 c0 t5 t0) (\lambda (x0: B).(\lambda (x1: C).(\lambda
-(x2: C).(\lambda (x3: T).(\lambda (H10: (eq C (CHead d (Bind Abbr) u) (CHead
-x1 (Bind x0) x3))).(\lambda (H11: (getl i c0 (CHead x2 (Bind x0)
-x3))).(\lambda (H12: (csubst0 (minus i0 (S i)) u0 x1 x2)).(let H13 \def
-(f_equal C C (\lambda (e0: C).(match e0 in C return (\lambda (_: C).C) with
-[(CSort _) \Rightarrow d | (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind
-Abbr) u) (CHead x1 (Bind x0) x3) H10) in ((let H14 \def (f_equal C B (\lambda
-(e0: C).(match e0 in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow
-Abbr | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with
-[(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr)
-u) (CHead x1 (Bind x0) x3) H10) in ((let H15 \def (f_equal C T (\lambda (e0:
-C).(match e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
-(CHead _ _ t6) \Rightarrow t6])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
-x3) H10) in (\lambda (H16: (eq B Abbr x0)).(\lambda (H17: (eq C d x1)).(let
-H18 \def (eq_ind_r T x3 (\lambda (t6: T).(getl i c0 (CHead x2 (Bind x0) t6)))
-H11 u H15) in (let H19 \def (eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus
-i0 (S i)) u0 c3 x2)) H12 d H17) in (let H20 \def (eq_ind_r B x0 (\lambda (b:
+T).(csubst0 (minus i0 (S i)) u0 e1 e2))))) (pc3 c0 t5 t0) (\lambda (x0:
+B).(\lambda (x1: C).(\lambda (x2: C).(\lambda (x3: T).(\lambda (H10: (eq C
+(CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3))).(\lambda (H11: (getl i c0
+(CHead x2 (Bind x0) x3))).(\lambda (H12: (csubst0 (minus i0 (S i)) u0 x1
+x2)).(let H13 \def (f_equal C C (\lambda (e0: C).(match e0 with [(CSort _)
+\Rightarrow d | (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u)
+(CHead x1 (Bind x0) x3) H10) in ((let H14 \def (f_equal C B (\lambda (e0:
+C).(match e0 with [(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow
+(match k with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead
+d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H10) in ((let H15 \def (f_equal C T
+(\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow u | (CHead _ _ t6)
+\Rightarrow t6])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H10) in
+(\lambda (H16: (eq B Abbr x0)).(\lambda (H17: (eq C d x1)).(let H18 \def
+(eq_ind_r T x3 (\lambda (t6: T).(getl i c0 (CHead x2 (Bind x0) t6))) H11 u
+H15) in (let H19 \def (eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus i0 (S
+i)) u0 c3 x2)) H12 d H17) in (let H20 \def (eq_ind_r B x0 (\lambda (b:
B).(getl i c0 (CHead x2 (Bind b) u))) H18 Abbr H16) in (pc3_pr2_u2 c0 t2 t5
(pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead e
(Bind Abbr) u0) H6) t2 t2 (pr0_refl t2) t5 H4) t0 (pc3_pr2_r c0 t2 t0
x1 (Bind x0) x3))).(\lambda (H11: (getl i c0 (CHead x2 (Bind x0)
x4))).(\lambda (H12: (subst0 (minus i0 (S i)) u0 x3 x4)).(\lambda (H13:
(csubst0 (minus i0 (S i)) u0 x1 x2)).(let H14 \def (f_equal C C (\lambda (e0:
-C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
-(CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
-x3) H10) in ((let H15 \def (f_equal C B (\lambda (e0: C).(match e0 in C
-return (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
-\Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
-x1 (Bind x0) x3) H10) in ((let H16 \def (f_equal C T (\lambda (e0: C).(match
-e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _
-t6) \Rightarrow t6])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H10) in
-(\lambda (H17: (eq B Abbr x0)).(\lambda (H18: (eq C d x1)).(let H19 \def
-(eq_ind_r T x3 (\lambda (t6: T).(subst0 (minus i0 (S i)) u0 t6 x4)) H12 u
-H16) in (let H20 \def (eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus i0 (S
-i)) u0 c3 x2)) H13 d H18) in (let H21 \def (eq_ind_r B x0 (\lambda (b:
-B).(getl i c0 (CHead x2 (Bind b) x4))) H11 Abbr H17) in (ex2_ind T (\lambda
-(t6: T).(subst0 i x4 t3 t6)) (\lambda (t6: T).(subst0 (S (plus (minus i0 (S
-i)) i)) u0 t0 t6)) (pc3 c0 t5 t0) (\lambda (x: T).(\lambda (H22: (subst0 i x4
-t3 x)).(\lambda (H23: (subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x)).(let
-H24 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i)) (\lambda (n:
-nat).(subst0 n u0 t0 x)) H23 i0 (lt_plus_minus_r i i0 H7)) in (pc3_pr2_u2 c0
-t2 t5 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5
-(CHead e (Bind Abbr) u0) H6) t2 t2 (pr0_refl t2) t5 H4) t0 (pc3_pr2_u c0 x t2
-(pr2_delta c0 x2 x4 i H21 t2 t3 H1 x H22) t0 (pc3_pr2_x c0 x t0 (pr2_delta c0
-e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead e (Bind Abbr) u0)
-H6) t0 t0 (pr0_refl t0) x H24)))))))) (subst0_subst0_back t3 t0 u i H2 x4 u0
-(minus i0 (S i)) H19)))))))) H15)) H14))))))))))) H9)) H8))) (\lambda (H7:
-(le i0 i)).(pc3_pr2_u2 c0 t2 t5 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0
-(le_n i0) c c0 u0 H5 (CHead e (Bind Abbr) u0) H6) t2 t2 (pr0_refl t2) t5 H4)
-t0 (pc3_pr2_r c0 t2 t0 (pr2_delta c0 d u i (csubst0_getl_ge i0 i H7 c c0 u0
-H5 (CHead d (Bind Abbr) u) H0) t2 t3 H1 t0 H2))))))))))) c2 t4
-H3)))))))))))))))) c1 t1 t H)))).
-(* COMMENTS
-Initial nodes: 6455
-END *)
+C).(match e0 with [(CSort _) \Rightarrow d | (CHead c3 _ _) \Rightarrow c3]))
+(CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H10) in ((let H15 \def
+(f_equal C B (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow Abbr |
+(CHead _ k _) \Rightarrow (match k with [(Bind b) \Rightarrow b | (Flat _)
+\Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H10) in
+((let H16 \def (f_equal C T (\lambda (e0: C).(match e0 with [(CSort _)
+\Rightarrow u | (CHead _ _ t6) \Rightarrow t6])) (CHead d (Bind Abbr) u)
+(CHead x1 (Bind x0) x3) H10) in (\lambda (H17: (eq B Abbr x0)).(\lambda (H18:
+(eq C d x1)).(let H19 \def (eq_ind_r T x3 (\lambda (t6: T).(subst0 (minus i0
+(S i)) u0 t6 x4)) H12 u H16) in (let H20 \def (eq_ind_r C x1 (\lambda (c3:
+C).(csubst0 (minus i0 (S i)) u0 c3 x2)) H13 d H18) in (let H21 \def (eq_ind_r
+B x0 (\lambda (b: B).(getl i c0 (CHead x2 (Bind b) x4))) H11 Abbr H17) in
+(ex2_ind T (\lambda (t6: T).(subst0 i x4 t3 t6)) (\lambda (t6: T).(subst0 (S
+(plus (minus i0 (S i)) i)) u0 t0 t6)) (pc3 c0 t5 t0) (\lambda (x: T).(\lambda
+(H22: (subst0 i x4 t3 x)).(\lambda (H23: (subst0 (S (plus (minus i0 (S i))
+i)) u0 t0 x)).(let H24 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i))
+(\lambda (n: nat).(subst0 n u0 t0 x)) H23 i0 (lt_plus_minus_r i i0 H7)) in
+(pc3_pr2_u2 c0 t2 t5 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c
+c0 u0 H5 (CHead e (Bind Abbr) u0) H6) t2 t2 (pr0_refl t2) t5 H4) t0
+(pc3_pr2_u c0 x t2 (pr2_delta c0 x2 x4 i H21 t2 t3 H1 x H22) t0 (pc3_pr2_x c0
+x t0 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead
+e (Bind Abbr) u0) H6) t0 t0 (pr0_refl t0) x H24)))))))) (subst0_subst0_back
+t3 t0 u i H2 x4 u0 (minus i0 (S i)) H19)))))))) H15)) H14))))))))))) H9))
+H8))) (\lambda (H7: (le i0 i)).(pc3_pr2_u2 c0 t2 t5 (pr2_delta c0 e u0 i0
+(csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead e (Bind Abbr) u0) H6) t2
+t2 (pr0_refl t2) t5 H4) t0 (pc3_pr2_r c0 t2 t0 (pr2_delta c0 d u i
+(csubst0_getl_ge i0 i H7 c c0 u0 H5 (CHead d (Bind Abbr) u) H0) t2 t3 H1 t0
+H2))))))))))) c2 t4 H3)))))))))))))))) c1 t1 t H)))).
-theorem pc3_pr2_fsubst0_back:
+lemma pc3_pr2_fsubst0_back:
\forall (c1: C).(\forall (t: T).(\forall (t1: T).((pr2 c1 t t1) \to (\forall
(i: nat).(\forall (u: T).(\forall (c2: C).(\forall (t2: T).((fsubst0 i u c1
t1 c2 t2) \to (\forall (e: C).((getl i c1 (CHead e (Bind Abbr) u)) \to (pc3
(x3: T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
x2))).(\lambda (H10: (getl i c0 (CHead x1 (Bind x0) x3))).(\lambda (H11:
(subst0 (minus i0 (S i)) u0 x2 x3)).(let H12 \def (f_equal C C (\lambda (e0:
-C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
-(CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
-x2) H9) in ((let H13 \def (f_equal C B (\lambda (e0: C).(match e0 in C return
-(\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
-\Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
-x1 (Bind x0) x2) H9) in ((let H14 \def (f_equal C T (\lambda (e0: C).(match
-e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _
-t5) \Rightarrow t5])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H9) in
-(\lambda (H15: (eq B Abbr x0)).(\lambda (H16: (eq C d x1)).(let H17 \def
-(eq_ind_r T x2 (\lambda (t5: T).(subst0 (minus i0 (S i)) u0 t5 x3)) H11 u
-H14) in (let H18 \def (eq_ind_r C x1 (\lambda (c3: C).(getl i c0 (CHead c3
-(Bind x0) x3))) H10 d H16) in (let H19 \def (eq_ind_r B x0 (\lambda (b:
-B).(getl i c0 (CHead d (Bind b) x3))) H18 Abbr H15) in (ex2_ind T (\lambda
-(t5: T).(subst0 i x3 t3 t5)) (\lambda (t5: T).(subst0 (S (plus (minus i0 (S
-i)) i)) u0 t0 t5)) (pc3 c0 t2 t0) (\lambda (x: T).(\lambda (H20: (subst0 i x3
-t3 x)).(\lambda (H21: (subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x)).(let
-H22 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i)) (\lambda (n:
-nat).(subst0 n u0 t0 x)) H21 i0 (lt_plus_minus_r i i0 H6)) in (pc3_pr2_u c0 x
-t2 (pr2_delta c0 d x3 i H19 t2 t3 H1 x H20) t0 (pc3_pr2_x c0 x t0 (pr2_delta
-c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H4 (CHead e (Bind Abbr)
-u0) H5) t0 t0 (pr0_refl t0) x H22))))))) (subst0_subst0_back t3 t0 u i H2 x3
-u0 (minus i0 (S i)) H17)))))))) H13)) H12))))))))) H8)) (\lambda (H8: (ex3_4
-B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq
-C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b:
-B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c0 (CHead e2
+C).(match e0 with [(CSort _) \Rightarrow d | (CHead c3 _ _) \Rightarrow c3]))
+(CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H9) in ((let H13 \def
+(f_equal C B (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow Abbr |
+(CHead _ k _) \Rightarrow (match k with [(Bind b) \Rightarrow b | (Flat _)
+\Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H9) in
+((let H14 \def (f_equal C T (\lambda (e0: C).(match e0 with [(CSort _)
+\Rightarrow u | (CHead _ _ t5) \Rightarrow t5])) (CHead d (Bind Abbr) u)
+(CHead x1 (Bind x0) x2) H9) in (\lambda (H15: (eq B Abbr x0)).(\lambda (H16:
+(eq C d x1)).(let H17 \def (eq_ind_r T x2 (\lambda (t5: T).(subst0 (minus i0
+(S i)) u0 t5 x3)) H11 u H14) in (let H18 \def (eq_ind_r C x1 (\lambda (c3:
+C).(getl i c0 (CHead c3 (Bind x0) x3))) H10 d H16) in (let H19 \def (eq_ind_r
+B x0 (\lambda (b: B).(getl i c0 (CHead d (Bind b) x3))) H18 Abbr H15) in
+(ex2_ind T (\lambda (t5: T).(subst0 i x3 t3 t5)) (\lambda (t5: T).(subst0 (S
+(plus (minus i0 (S i)) i)) u0 t0 t5)) (pc3 c0 t2 t0) (\lambda (x: T).(\lambda
+(H20: (subst0 i x3 t3 x)).(\lambda (H21: (subst0 (S (plus (minus i0 (S i))
+i)) u0 t0 x)).(let H22 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i))
+(\lambda (n: nat).(subst0 n u0 t0 x)) H21 i0 (lt_plus_minus_r i i0 H6)) in
+(pc3_pr2_u c0 x t2 (pr2_delta c0 d x3 i H19 t2 t3 H1 x H20) t0 (pc3_pr2_x c0
+x t0 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H4 (CHead
+e (Bind Abbr) u0) H5) t0 t0 (pr0_refl t0) x H22))))))) (subst0_subst0_back t3
+t0 u i H2 x3 u0 (minus i0 (S i)) H17)))))))) H13)) H12))))))))) H8)) (\lambda
+(H8: (ex3_4 B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda
+(u1: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda
+(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c0 (CHead e2
(Bind b) u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda
(_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))).(ex3_4_ind B C C T (\lambda
(b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind
(x2: C).(\lambda (x3: T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead
x1 (Bind x0) x3))).(\lambda (H10: (getl i c0 (CHead x2 (Bind x0)
x3))).(\lambda (H11: (csubst0 (minus i0 (S i)) u0 x1 x2)).(let H12 \def
-(f_equal C C (\lambda (e0: C).(match e0 in C return (\lambda (_: C).C) with
-[(CSort _) \Rightarrow d | (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind
-Abbr) u) (CHead x1 (Bind x0) x3) H9) in ((let H13 \def (f_equal C B (\lambda
-(e0: C).(match e0 in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow
-Abbr | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with
-[(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr)
-u) (CHead x1 (Bind x0) x3) H9) in ((let H14 \def (f_equal C T (\lambda (e0:
-C).(match e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
-(CHead _ _ t5) \Rightarrow t5])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
-x3) H9) in (\lambda (H15: (eq B Abbr x0)).(\lambda (H16: (eq C d x1)).(let
-H17 \def (eq_ind_r T x3 (\lambda (t5: T).(getl i c0 (CHead x2 (Bind x0) t5)))
-H10 u H14) in (let H18 \def (eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus
-i0 (S i)) u0 c3 x2)) H11 d H16) in (let H19 \def (eq_ind_r B x0 (\lambda (b:
-B).(getl i c0 (CHead x2 (Bind b) u))) H17 Abbr H15) in (pc3_pr2_r c0 t2 t0
-(pr2_delta c0 x2 u i H19 t2 t3 H1 t0 H2)))))))) H13)) H12))))))))) H8))
-(\lambda (H8: (ex4_5 B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1
-(Bind b) u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda
-(_: T).(\lambda (w: T).(getl i c0 (CHead e2 (Bind b) w))))))) (\lambda (_:
-B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
-(minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1
-e2)))))))).(ex4_5_ind B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1
-(Bind b) u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda
-(_: T).(\lambda (w: T).(getl i c0 (CHead e2 (Bind b) w))))))) (\lambda (_:
-B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
-(minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))
-(pc3 c0 t2 t0) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: C).(\lambda
-(x3: T).(\lambda (x4: T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead
-x1 (Bind x0) x3))).(\lambda (H10: (getl i c0 (CHead x2 (Bind x0)
-x4))).(\lambda (H11: (subst0 (minus i0 (S i)) u0 x3 x4)).(\lambda (H12:
-(csubst0 (minus i0 (S i)) u0 x1 x2)).(let H13 \def (f_equal C C (\lambda (e0:
-C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
+(f_equal C C (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow d |
(CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
-x3) H9) in ((let H14 \def (f_equal C B (\lambda (e0: C).(match e0 in C return
-(\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
-\Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
-x1 (Bind x0) x3) H9) in ((let H15 \def (f_equal C T (\lambda (e0: C).(match
-e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _
-t5) \Rightarrow t5])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in
+x3) H9) in ((let H13 \def (f_equal C B (\lambda (e0: C).(match e0 with
+[(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow (match k with [(Bind
+b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u)
+(CHead x1 (Bind x0) x3) H9) in ((let H14 \def (f_equal C T (\lambda (e0:
+C).(match e0 with [(CSort _) \Rightarrow u | (CHead _ _ t5) \Rightarrow t5]))
+(CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in (\lambda (H15: (eq B
+Abbr x0)).(\lambda (H16: (eq C d x1)).(let H17 \def (eq_ind_r T x3 (\lambda
+(t5: T).(getl i c0 (CHead x2 (Bind x0) t5))) H10 u H14) in (let H18 \def
+(eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus i0 (S i)) u0 c3 x2)) H11 d
+H16) in (let H19 \def (eq_ind_r B x0 (\lambda (b: B).(getl i c0 (CHead x2
+(Bind b) u))) H17 Abbr H15) in (pc3_pr2_r c0 t2 t0 (pr2_delta c0 x2 u i H19
+t2 t3 H1 t0 H2)))))))) H13)) H12))))))))) H8)) (\lambda (H8: (ex4_5 B C C T T
+(\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
+(_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1))))))) (\lambda
+(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl
+i c0 (CHead e2 (Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1 w))))))
+(\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 (minus i0 (S i)) u0 e1 e2)))))))).(ex4_5_ind B C C T T
+(\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
+(_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1))))))) (\lambda
+(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl
+i c0 (CHead e2 (Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1 w))))))
+(\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 (minus i0 (S i)) u0 e1 e2)))))) (pc3 c0 t2 t0) (\lambda (x0:
+B).(\lambda (x1: C).(\lambda (x2: C).(\lambda (x3: T).(\lambda (x4:
+T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
+x3))).(\lambda (H10: (getl i c0 (CHead x2 (Bind x0) x4))).(\lambda (H11:
+(subst0 (minus i0 (S i)) u0 x3 x4)).(\lambda (H12: (csubst0 (minus i0 (S i))
+u0 x1 x2)).(let H13 \def (f_equal C C (\lambda (e0: C).(match e0 with [(CSort
+_) \Rightarrow d | (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u)
+(CHead x1 (Bind x0) x3) H9) in ((let H14 \def (f_equal C B (\lambda (e0:
+C).(match e0 with [(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow
+(match k with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead
+d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in ((let H15 \def (f_equal C T
+(\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow u | (CHead _ _ t5)
+\Rightarrow t5])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in
(\lambda (H16: (eq B Abbr x0)).(\lambda (H17: (eq C d x1)).(let H18 \def
(eq_ind_r T x3 (\lambda (t5: T).(subst0 (minus i0 (S i)) u0 t5 x4)) H11 u
H15) in (let H19 \def (eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus i0 (S
T).(\lambda (x3: T).(\lambda (H10: (eq C (CHead d (Bind Abbr) u) (CHead x1
(Bind x0) x2))).(\lambda (H11: (getl i c0 (CHead x1 (Bind x0) x3))).(\lambda
(H12: (subst0 (minus i0 (S i)) u0 x2 x3)).(let H13 \def (f_equal C C (\lambda
-(e0: C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow
-d | (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind
-x0) x2) H10) in ((let H14 \def (f_equal C B (\lambda (e0: C).(match e0 in C
-return (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
-\Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
-x1 (Bind x0) x2) H10) in ((let H15 \def (f_equal C T (\lambda (e0: C).(match
-e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _
-t6) \Rightarrow t6])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H10) in
-(\lambda (H16: (eq B Abbr x0)).(\lambda (H17: (eq C d x1)).(let H18 \def
-(eq_ind_r T x2 (\lambda (t6: T).(subst0 (minus i0 (S i)) u0 t6 x3)) H12 u
-H15) in (let H19 \def (eq_ind_r C x1 (\lambda (c3: C).(getl i c0 (CHead c3
-(Bind x0) x3))) H11 d H17) in (let H20 \def (eq_ind_r B x0 (\lambda (b:
-B).(getl i c0 (CHead d (Bind b) x3))) H19 Abbr H16) in (ex2_ind T (\lambda
-(t6: T).(subst0 i x3 t3 t6)) (\lambda (t6: T).(subst0 (S (plus (minus i0 (S
-i)) i)) u0 t0 t6)) (pc3 c0 t2 t5) (\lambda (x: T).(\lambda (H21: (subst0 i x3
-t3 x)).(\lambda (H22: (subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x)).(let
-H23 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i)) (\lambda (n:
-nat).(subst0 n u0 t0 x)) H22 i0 (lt_plus_minus_r i i0 H7)) in (pc3_pr2_u c0 x
-t2 (pr2_delta c0 d x3 i H20 t2 t3 H1 x H21) t5 (pc3_pr2_u2 c0 t0 x (pr2_delta
-c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead e (Bind Abbr)
-u0) H6) t0 t0 (pr0_refl t0) x H23) t5 (pc3_pr2_r c0 t0 t5 (pr2_delta c0 e u0
-i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead e (Bind Abbr) u0) H6)
-t0 t0 (pr0_refl t0) t5 H4)))))))) (subst0_subst0_back t3 t0 u i H2 x3 u0
-(minus i0 (S i)) H18)))))))) H14)) H13))))))))) H9)) (\lambda (H9: (ex3_4 B C
-C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C
-(CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: B).(\lambda
-(_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c0 (CHead e2 (Bind b)
-u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
-T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))).(ex3_4_ind B C C T (\lambda (b:
-B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind
+(e0: C).(match e0 with [(CSort _) \Rightarrow d | (CHead c3 _ _) \Rightarrow
+c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H10) in ((let H14 \def
+(f_equal C B (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow Abbr |
+(CHead _ k _) \Rightarrow (match k with [(Bind b) \Rightarrow b | (Flat _)
+\Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H10) in
+((let H15 \def (f_equal C T (\lambda (e0: C).(match e0 with [(CSort _)
+\Rightarrow u | (CHead _ _ t6) \Rightarrow t6])) (CHead d (Bind Abbr) u)
+(CHead x1 (Bind x0) x2) H10) in (\lambda (H16: (eq B Abbr x0)).(\lambda (H17:
+(eq C d x1)).(let H18 \def (eq_ind_r T x2 (\lambda (t6: T).(subst0 (minus i0
+(S i)) u0 t6 x3)) H12 u H15) in (let H19 \def (eq_ind_r C x1 (\lambda (c3:
+C).(getl i c0 (CHead c3 (Bind x0) x3))) H11 d H17) in (let H20 \def (eq_ind_r
+B x0 (\lambda (b: B).(getl i c0 (CHead d (Bind b) x3))) H19 Abbr H16) in
+(ex2_ind T (\lambda (t6: T).(subst0 i x3 t3 t6)) (\lambda (t6: T).(subst0 (S
+(plus (minus i0 (S i)) i)) u0 t0 t6)) (pc3 c0 t2 t5) (\lambda (x: T).(\lambda
+(H21: (subst0 i x3 t3 x)).(\lambda (H22: (subst0 (S (plus (minus i0 (S i))
+i)) u0 t0 x)).(let H23 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i))
+(\lambda (n: nat).(subst0 n u0 t0 x)) H22 i0 (lt_plus_minus_r i i0 H7)) in
+(pc3_pr2_u c0 x t2 (pr2_delta c0 d x3 i H20 t2 t3 H1 x H21) t5 (pc3_pr2_u2 c0
+t0 x (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead
+e (Bind Abbr) u0) H6) t0 t0 (pr0_refl t0) x H23) t5 (pc3_pr2_r c0 t0 t5
+(pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead e
+(Bind Abbr) u0) H6) t0 t0 (pr0_refl t0) t5 H4)))))))) (subst0_subst0_back t3
+t0 u i H2 x3 u0 (minus i0 (S i)) H18)))))))) H14)) H13))))))))) H9)) (\lambda
+(H9: (ex3_4 B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda
+(u1: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda
+(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c0 (CHead e2
+(Bind b) u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda
+(_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))).(ex3_4_ind B C C T (\lambda
+(b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind
Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: B).(\lambda (_: C).(\lambda
(e2: C).(\lambda (u1: T).(getl i c0 (CHead e2 (Bind b) u1)))))) (\lambda (_:
B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus i0 (S
(x2: C).(\lambda (x3: T).(\lambda (H10: (eq C (CHead d (Bind Abbr) u) (CHead
x1 (Bind x0) x3))).(\lambda (H11: (getl i c0 (CHead x2 (Bind x0)
x3))).(\lambda (H12: (csubst0 (minus i0 (S i)) u0 x1 x2)).(let H13 \def
-(f_equal C C (\lambda (e0: C).(match e0 in C return (\lambda (_: C).C) with
-[(CSort _) \Rightarrow d | (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind
-Abbr) u) (CHead x1 (Bind x0) x3) H10) in ((let H14 \def (f_equal C B (\lambda
-(e0: C).(match e0 in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow
-Abbr | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with
-[(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr)
-u) (CHead x1 (Bind x0) x3) H10) in ((let H15 \def (f_equal C T (\lambda (e0:
-C).(match e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
-(CHead _ _ t6) \Rightarrow t6])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
-x3) H10) in (\lambda (H16: (eq B Abbr x0)).(\lambda (H17: (eq C d x1)).(let
-H18 \def (eq_ind_r T x3 (\lambda (t6: T).(getl i c0 (CHead x2 (Bind x0) t6)))
-H11 u H15) in (let H19 \def (eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus
-i0 (S i)) u0 c3 x2)) H12 d H17) in (let H20 \def (eq_ind_r B x0 (\lambda (b:
-B).(getl i c0 (CHead x2 (Bind b) u))) H18 Abbr H16) in (pc3_pr2_u c0 t0 t2
-(pr2_delta c0 x2 u i H20 t2 t3 H1 t0 H2) t5 (pc3_pr2_r c0 t0 t5 (pr2_delta c0
-e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead e (Bind Abbr) u0)
-H6) t0 t0 (pr0_refl t0) t5 H4))))))))) H14)) H13))))))))) H9)) (\lambda (H9:
-(ex4_5 B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda
-(u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b)
-u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
-T).(\lambda (w: T).(getl i c0 (CHead e2 (Bind b) w))))))) (\lambda (_:
-B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
-(minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1
-e2)))))))).(ex4_5_ind B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1
-(Bind b) u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda
-(_: T).(\lambda (w: T).(getl i c0 (CHead e2 (Bind b) w))))))) (\lambda (_:
-B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
-(minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))
-(pc3 c0 t2 t5) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: C).(\lambda
-(x3: T).(\lambda (x4: T).(\lambda (H10: (eq C (CHead d (Bind Abbr) u) (CHead
-x1 (Bind x0) x3))).(\lambda (H11: (getl i c0 (CHead x2 (Bind x0)
-x4))).(\lambda (H12: (subst0 (minus i0 (S i)) u0 x3 x4)).(\lambda (H13:
-(csubst0 (minus i0 (S i)) u0 x1 x2)).(let H14 \def (f_equal C C (\lambda (e0:
-C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
+(f_equal C C (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow d |
(CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
-x3) H10) in ((let H15 \def (f_equal C B (\lambda (e0: C).(match e0 in C
-return (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
-\Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
-x1 (Bind x0) x3) H10) in ((let H16 \def (f_equal C T (\lambda (e0: C).(match
-e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _
-t6) \Rightarrow t6])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H10) in
+x3) H10) in ((let H14 \def (f_equal C B (\lambda (e0: C).(match e0 with
+[(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow (match k with [(Bind
+b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u)
+(CHead x1 (Bind x0) x3) H10) in ((let H15 \def (f_equal C T (\lambda (e0:
+C).(match e0 with [(CSort _) \Rightarrow u | (CHead _ _ t6) \Rightarrow t6]))
+(CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H10) in (\lambda (H16: (eq B
+Abbr x0)).(\lambda (H17: (eq C d x1)).(let H18 \def (eq_ind_r T x3 (\lambda
+(t6: T).(getl i c0 (CHead x2 (Bind x0) t6))) H11 u H15) in (let H19 \def
+(eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus i0 (S i)) u0 c3 x2)) H12 d
+H17) in (let H20 \def (eq_ind_r B x0 (\lambda (b: B).(getl i c0 (CHead x2
+(Bind b) u))) H18 Abbr H16) in (pc3_pr2_u c0 t0 t2 (pr2_delta c0 x2 u i H20
+t2 t3 H1 t0 H2) t5 (pc3_pr2_r c0 t0 t5 (pr2_delta c0 e u0 i0 (csubst0_getl_ge
+i0 i0 (le_n i0) c c0 u0 H5 (CHead e (Bind Abbr) u0) H6) t0 t0 (pr0_refl t0)
+t5 H4))))))))) H14)) H13))))))))) H9)) (\lambda (H9: (ex4_5 B C C T T
+(\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
+(_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1))))))) (\lambda
+(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl
+i c0 (CHead e2 (Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1 w))))))
+(\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 (minus i0 (S i)) u0 e1 e2)))))))).(ex4_5_ind B C C T T
+(\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
+(_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1))))))) (\lambda
+(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl
+i c0 (CHead e2 (Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1 w))))))
+(\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 (minus i0 (S i)) u0 e1 e2)))))) (pc3 c0 t2 t5) (\lambda (x0:
+B).(\lambda (x1: C).(\lambda (x2: C).(\lambda (x3: T).(\lambda (x4:
+T).(\lambda (H10: (eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
+x3))).(\lambda (H11: (getl i c0 (CHead x2 (Bind x0) x4))).(\lambda (H12:
+(subst0 (minus i0 (S i)) u0 x3 x4)).(\lambda (H13: (csubst0 (minus i0 (S i))
+u0 x1 x2)).(let H14 \def (f_equal C C (\lambda (e0: C).(match e0 with [(CSort
+_) \Rightarrow d | (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u)
+(CHead x1 (Bind x0) x3) H10) in ((let H15 \def (f_equal C B (\lambda (e0:
+C).(match e0 with [(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow
+(match k with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead
+d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H10) in ((let H16 \def (f_equal C T
+(\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow u | (CHead _ _ t6)
+\Rightarrow t6])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H10) in
(\lambda (H17: (eq B Abbr x0)).(\lambda (H18: (eq C d x1)).(let H19 \def
(eq_ind_r T x3 (\lambda (t6: T).(subst0 (minus i0 (S i)) u0 t6 x4)) H12 u
H16) in (let H20 \def (eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus i0 (S
H2) t5 (pc3_pr2_r c0 t0 t5 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n
i0) c c0 u0 H5 (CHead e (Bind Abbr) u0) H6) t0 t0 (pr0_refl t0) t5
H4))))))))))) c2 t4 H3)))))))))))))))) c1 t t1 H)))).
-(* COMMENTS
-Initial nodes: 6191
-END *)
-theorem pc3_fsubst0:
+lemma pc3_fsubst0:
\forall (c1: C).(\forall (t1: T).(\forall (t: T).((pc3 c1 t1 t) \to (\forall
(i: nat).(\forall (u: T).(\forall (c2: C).(\forall (t2: T).((fsubst0 i u c1
t1 c2 t2) \to (\forall (e: C).((getl i c1 (CHead e (Bind Abbr) u)) \to (pc3
u))).(pc3_t t0 c0 t5 (pc3_s c0 t5 t0 (pc3_pr2_fsubst0_back c1 t0 t2 H0 i u c0
t5 (fsubst0_both i u c1 t2 t5 H4 c0 H5) e H6)) t3 (H2 i u c0 t0 (fsubst0_fst
i u c1 t0 c0 H5) e H6)))))))) c2 t4 H3)))))))))))) t1 t H)))).
-(* COMMENTS
-Initial nodes: 1249
-END *)
projects / helm.git / blobdiff