(* This file was automatically generated: do not edit *********************)
-include "Basic-1/subst0/fwd.ma".
+include "basic_1/subst0/fwd.ma".
-theorem subst0_refl:
+lemma subst0_refl:
\forall (u: T).(\forall (t: T).(\forall (d: nat).((subst0 d u t t) \to
(\forall (P: Prop).P))))
\def
u2)))).(ex2_ind T (\lambda (u2: T).(eq T (THead k t0 t1) (THead k u2 t1)))
(\lambda (u2: T).(subst0 d u t0 u2)) P (\lambda (x: T).(\lambda (H3: (eq T
(THead k t0 t1) (THead k x t1))).(\lambda (H4: (subst0 d u t0 x)).(let H5
-\def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
-with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ t2 _)
-\Rightarrow t2])) (THead k t0 t1) (THead k x t1) H3) in (let H6 \def
-(eq_ind_r T x (\lambda (t2: T).(subst0 d u t0 t2)) H4 t0 H5) in (H d H6
-P)))))) H2)) (\lambda (H2: (ex2 T (\lambda (t2: T).(eq T (THead k t0 t1)
-(THead k t0 t2))) (\lambda (t2: T).(subst0 (s k d) u t1 t2)))).(ex2_ind T
-(\lambda (t2: T).(eq T (THead k t0 t1) (THead k t0 t2))) (\lambda (t2:
-T).(subst0 (s k d) u t1 t2)) P (\lambda (x: T).(\lambda (H3: (eq T (THead k
-t0 t1) (THead k t0 x))).(\lambda (H4: (subst0 (s k d) u t1 x)).(let H5 \def
-(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with
-[(TSort _) \Rightarrow t1 | (TLRef _) \Rightarrow t1 | (THead _ _ t2)
-\Rightarrow t2])) (THead k t0 t1) (THead k t0 x) H3) in (let H6 \def
-(eq_ind_r T x (\lambda (t2: T).(subst0 (s k d) u t1 t2)) H4 t1 H5) in (H0 (s
-k d) H6 P)))))) H2)) (\lambda (H2: (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
-T).(eq T (THead k t0 t1) (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_:
-T).(subst0 d u t0 u2))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k d) u t1
-t2))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead k t0
+\def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow t0 |
+(TLRef _) \Rightarrow t0 | (THead _ t2 _) \Rightarrow t2])) (THead k t0 t1)
+(THead k x t1) H3) in (let H6 \def (eq_ind_r T x (\lambda (t2: T).(subst0 d u
+t0 t2)) H4 t0 H5) in (H d H6 P)))))) H2)) (\lambda (H2: (ex2 T (\lambda (t2:
+T).(eq T (THead k t0 t1) (THead k t0 t2))) (\lambda (t2: T).(subst0 (s k d) u
+t1 t2)))).(ex2_ind T (\lambda (t2: T).(eq T (THead k t0 t1) (THead k t0 t2)))
+(\lambda (t2: T).(subst0 (s k d) u t1 t2)) P (\lambda (x: T).(\lambda (H3:
+(eq T (THead k t0 t1) (THead k t0 x))).(\lambda (H4: (subst0 (s k d) u t1
+x)).(let H5 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
+\Rightarrow t1 | (TLRef _) \Rightarrow t1 | (THead _ _ t2) \Rightarrow t2]))
+(THead k t0 t1) (THead k t0 x) H3) in (let H6 \def (eq_ind_r T x (\lambda
+(t2: T).(subst0 (s k d) u t1 t2)) H4 t1 H5) in (H0 (s k d) H6 P)))))) H2))
+(\lambda (H2: (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead k t0
t1) (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(subst0 d u t0 u2)))
-(\lambda (_: T).(\lambda (t2: T).(subst0 (s k d) u t1 t2))) P (\lambda (x0:
-T).(\lambda (x1: T).(\lambda (H3: (eq T (THead k t0 t1) (THead k x0
-x1))).(\lambda (H4: (subst0 d u t0 x0)).(\lambda (H5: (subst0 (s k d) u t1
-x1)).(let H6 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda
-(_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead
-_ t2 _) \Rightarrow t2])) (THead k t0 t1) (THead k x0 x1) H3) in ((let H7
-\def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
-with [(TSort _) \Rightarrow t1 | (TLRef _) \Rightarrow t1 | (THead _ _ t2)
+(\lambda (_: T).(\lambda (t2: T).(subst0 (s k d) u t1 t2))))).(ex3_2_ind T T
+(\lambda (u2: T).(\lambda (t2: T).(eq T (THead k t0 t1) (THead k u2 t2))))
+(\lambda (u2: T).(\lambda (_: T).(subst0 d u t0 u2))) (\lambda (_:
+T).(\lambda (t2: T).(subst0 (s k d) u t1 t2))) P (\lambda (x0: T).(\lambda
+(x1: T).(\lambda (H3: (eq T (THead k t0 t1) (THead k x0 x1))).(\lambda (H4:
+(subst0 d u t0 x0)).(\lambda (H5: (subst0 (s k d) u t1 x1)).(let H6 \def
+(f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow t0 | (TLRef
+_) \Rightarrow t0 | (THead _ t2 _) \Rightarrow t2])) (THead k t0 t1) (THead k
+x0 x1) H3) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e with
+[(TSort _) \Rightarrow t1 | (TLRef _) \Rightarrow t1 | (THead _ _ t2)
\Rightarrow t2])) (THead k t0 t1) (THead k x0 x1) H3) in (\lambda (H8: (eq T
t0 x0)).(let H9 \def (eq_ind_r T x1 (\lambda (t2: T).(subst0 (s k d) u t1
t2)) H5 t1 H7) in (let H10 \def (eq_ind_r T x0 (\lambda (t2: T).(subst0 d u
t0 t2)) H4 t0 H8) in (H d H10 P))))) H6))))))) H2)) (subst0_gen_head k u t0
t1 (THead k t0 t1) d H1)))))))))) t)).
-(* COMMENTS
-Initial nodes: 1119
-END *)
-theorem subst0_lift_lt:
+lemma subst0_lift_lt:
\forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst0
i u t1 t2) \to (\forall (d: nat).((lt i d) \to (\forall (h: nat).(subst0 i
(lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)))))))))
(s_lt k i0 d H4) h) (minus d (S i0)) (minus_s_s k d (S i0)))) (lift h d
(THead k u2 t3)) (lift_head k u2 t3 h d)) (lift h d (THead k u1 t0))
(lift_head k u1 t0 h d))))))))))))))))) i u t1 t2 H))))).
-(* COMMENTS
-Initial nodes: 1805
-END *)
-theorem subst0_lift_ge:
+lemma subst0_lift_ge:
\forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).(\forall
(h: nat).((subst0 i u t1 t2) \to (\forall (d: nat).((le d i) \to (subst0
(plus i h) u (lift h d t1) (lift h d t2)))))))))
h) (H1 d H4) k (lift h (s k d) t0) (lift h (s k d) t3) (H5 (s k d) (s_le k d
i0 H4))) (lift h d (THead k u2 t3)) (lift_head k u2 t3 h d)) (lift h d (THead
k u1 t0)) (lift_head k u1 t0 h d)))))))))))))))) i u t1 t2 H)))))).
-(* COMMENTS
-Initial nodes: 1449
-END *)
-theorem subst0_lift_ge_S:
+lemma subst0_lift_ge_S:
\forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst0
i u t1 t2) \to (\forall (d: nat).((le d i) \to (subst0 (S i) u (lift (S O) d
t1) (lift (S O) d t2))))))))
(H: (subst0 i u t1 t2)).(\lambda (d: nat).(\lambda (H0: (le d i)).(eq_ind nat
(plus i (S O)) (\lambda (n: nat).(subst0 n u (lift (S O) d t1) (lift (S O) d
t2))) (subst0_lift_ge t1 t2 u i (S O) H d H0) (S i) (eq_ind_r nat (plus (S O)
-i) (\lambda (n: nat).(eq nat n (S i))) (refl_equal nat (S i)) (plus i (S O))
-(plus_sym i (S O)))))))))).
-(* COMMENTS
-Initial nodes: 137
-END *)
+i) (\lambda (n: nat).(eq nat n (S i))) (le_antisym (plus (S O) i) (S i) (le_n
+(S i)) (le_n (plus (S O) i))) (plus i (S O)) (plus_sym i (S O)))))))))).
-theorem subst0_lift_ge_s:
+lemma subst0_lift_ge_s:
\forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst0
i u t1 t2) \to (\forall (d: nat).((le d i) \to (\forall (b: B).(subst0 (s
(Bind b) i) u (lift (S O) d t1) (lift (S O) d t2)))))))))
\lambda (t1: T).(\lambda (t2: T).(\lambda (u: T).(\lambda (i: nat).(\lambda
(H: (subst0 i u t1 t2)).(\lambda (d: nat).(\lambda (H0: (le d i)).(\lambda
(_: B).(subst0_lift_ge_S t1 t2 u i H d H0)))))))).
-(* COMMENTS
-Initial nodes: 43
-END *)