X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fsubst1%2Fprops.ma;h=f7bf1d15cdc3c14635c2374e49a90cdaaf6de2ad;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=ac8dea954a58cf9a878caf8362c6b88de0fcaa10;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/subst1/props.ma b/matita/matita/contribs/lambdadelta/basic_1/subst1/props.ma
index ac8dea954..f7bf1d15c 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/subst1/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/subst1/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/subst1/defs.ma".
+include "basic_1/subst1/fwd.ma".
 
-include "Basic-1/subst0/props.ma".
+include "basic_1/subst0/props.ma".
 
 theorem subst1_head:
  \forall (v: T).(\forall (u1: T).(\forall (u2: T).(\forall (i: nat).((subst1 
@@ -38,11 +38,8 @@ k u1 t1) (THead k t2 t))) (subst1_single i v (THead k u1 t1) (THead k t2 t1)
 (subst0_fst v t2 u1 i H0 t1 k)) (\lambda (t3: T).(\lambda (H2: (subst0 (s k 
 i) v t1 t3)).(subst1_single i v (THead k u1 t1) (THead k t2 t3) (subst0_both 
 v u1 t2 i H0 k t1 t3 H2)))) t0 H1))))))) u2 H))))).
-(* COMMENTS
-Initial nodes: 369
-END *)
 
-theorem subst1_lift_lt:
+lemma subst1_lift_lt:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst1 
 i u t1 t2) \to (\forall (d: nat).((lt i d) \to (\forall (h: nat).(subst1 i 
 (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)))))))))
@@ -56,11 +53,8 @@ t1))))) (\lambda (t3: T).(\lambda (H0: (subst0 i u t1 t3)).(\lambda (d:
 nat).(\lambda (H1: (lt i d)).(\lambda (h: nat).(subst1_single i (lift h 
 (minus d (S i)) u) (lift h d t1) (lift h d t3) (subst0_lift_lt t1 t3 u i H0 d 
 H1 h))))))) t2 H))))).
-(* COMMENTS
-Initial nodes: 185
-END *)
 
-theorem subst1_lift_ge:
+lemma subst1_lift_ge:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).(\forall 
 (h: nat).((subst1 i u t1 t2) \to (\forall (d: nat).((le d i) \to (subst1 
 (plus i h) u (lift h d t1) (lift h d t2)))))))))
@@ -72,11 +66,8 @@ d t))))) (\lambda (d: nat).(\lambda (_: (le d i)).(subst1_refl (plus i h) u
 (lift h d t1)))) (\lambda (t3: T).(\lambda (H0: (subst0 i u t1 t3)).(\lambda 
 (d: nat).(\lambda (H1: (le d i)).(subst1_single (plus i h) u (lift h d t1) 
 (lift h d t3) (subst0_lift_ge t1 t3 u i h H0 d H1)))))) t2 H)))))).
-(* COMMENTS
-Initial nodes: 157
-END *)
 
-theorem subst1_ex:
+lemma subst1_ex:
  \forall (u: T).(\forall (t1: T).(\forall (d: nat).(ex T (\lambda (t2: 
 T).(subst1 d u t1 (lift (S O) d t2))))))
 \def
@@ -95,7 +86,7 @@ O) d H)))) (\lambda (H: (eq nat n d)).(eq_ind nat n (\lambda (n0: nat).(ex T
 (\lambda (t2: T).(subst1 n u (TLRef n) (lift (S O) n t2))) (lift n O u) 
 (eq_ind_r T (lift (plus (S O) n) O u) (\lambda (t: T).(subst1 n u (TLRef n) 
 t)) (subst1_single n u (TLRef n) (lift (S n) O u) (subst0_lref u n)) (lift (S 
-O) n (lift n O u)) (lift_free u n (S O) O n (le_n (plus O n)) (le_O_n n)))) d 
+O) n (lift n O u)) (lift_free u n (S O) O n (le_plus_r O n) (le_O_n n)))) d 
 H)) (\lambda (H: (lt d n)).(ex_intro T (\lambda (t2: T).(subst1 d u (TLRef n) 
 (lift (S O) d t2))) (TLRef (pred n)) (eq_ind_r T (TLRef n) (\lambda (t: 
 T).(subst1 d u (TLRef n) t)) (subst1_refl d u (TLRef n)) (lift (S O) d (TLRef 
@@ -115,11 +106,8 @@ t2))) (THead k x x0) (eq_ind_r T (THead k (lift (S O) d x) (lift (S O) (s k
 d) x0)) (\lambda (t2: T).(subst1 d u (THead k t t0) t2)) (subst1_head u t 
 (lift (S O) d x) d H2 k t0 (lift (S O) (s k d) x0) H4) (lift (S O) d (THead k 
 x x0)) (lift_head k x x0 (S O) d))))) H3))))) H1))))))))) t1)).
-(* COMMENTS
-Initial nodes: 925
-END *)
 
-theorem subst1_lift_S:
+lemma subst1_lift_S:
  \forall (u: T).(\forall (i: nat).(\forall (h: nat).((le h i) \to (subst1 i 
 (TLRef h) (lift (S h) (S i) u) (lift (S h) i u)))))
 \def
@@ -136,29 +124,30 @@ i))))))) (\lambda (n: nat).(\lambda (i: nat).(\lambda (h: nat).(\lambda (H:
 (\lambda (t: T).(subst1 i (TLRef h) t (lift (S h) i (TLRef n)))) (eq_ind_r T 
 (TLRef n) (\lambda (t: T).(subst1 i (TLRef h) (TLRef n) t)) (subst1_refl i 
 (TLRef h) (TLRef n)) (lift (S h) i (TLRef n)) (lift_lref_lt n (S h) i H0)) 
-(lift (S h) (S i) (TLRef n)) (lift_lref_lt n (S h) (S i) (le_S (S n) i H0)))) 
-(\lambda (H0: (eq nat n i)).(let H1 \def (eq_ind_r nat i (\lambda (n0: 
-nat).(le h n0)) H n H0) in (eq_ind nat n (\lambda (n0: nat).(subst1 n0 (TLRef 
-h) (lift (S h) (S n0) (TLRef n)) (lift (S h) n0 (TLRef n)))) (eq_ind_r T 
-(TLRef n) (\lambda (t: T).(subst1 n (TLRef h) t (lift (S h) n (TLRef n)))) 
-(eq_ind_r T (TLRef (plus n (S h))) (\lambda (t: T).(subst1 n (TLRef h) (TLRef 
-n) t)) (eq_ind nat (S (plus n h)) (\lambda (n0: nat).(subst1 n (TLRef h) 
-(TLRef n) (TLRef n0))) (eq_ind_r nat (plus h n) (\lambda (n0: nat).(subst1 n 
-(TLRef h) (TLRef n) (TLRef (S n0)))) (eq_ind nat (plus h (S n)) (\lambda (n0: 
-nat).(subst1 n (TLRef h) (TLRef n) (TLRef n0))) (eq_ind T (lift (S n) O 
-(TLRef h)) (\lambda (t: T).(subst1 n (TLRef h) (TLRef n) t)) (subst1_single n 
-(TLRef h) (TLRef n) (lift (S n) O (TLRef h)) (subst0_lref (TLRef h) n)) 
-(TLRef (plus h (S n))) (lift_lref_ge h (S n) O (le_O_n h))) (S (plus h n)) 
-(sym_eq nat (S (plus h n)) (plus h (S n)) (plus_n_Sm h n))) (plus n h) 
-(plus_sym n h)) (plus n (S h)) (plus_n_Sm n h)) (lift (S h) n (TLRef n)) 
-(lift_lref_ge n (S h) n (le_n n))) (lift (S h) (S n) (TLRef n)) (lift_lref_lt 
-n (S h) (S n) (le_n (S n)))) i H0))) (\lambda (H0: (lt i n)).(eq_ind_r T 
-(TLRef (plus n (S h))) (\lambda (t: T).(subst1 i (TLRef h) t (lift (S h) i 
-(TLRef n)))) (eq_ind_r T (TLRef (plus n (S h))) (\lambda (t: T).(subst1 i 
-(TLRef h) (TLRef (plus n (S h))) t)) (subst1_refl i (TLRef h) (TLRef (plus n 
-(S h)))) (lift (S h) i (TLRef n)) (lift_lref_ge n (S h) i (le_S_n i n (le_S 
-(S i) n H0)))) (lift (S h) (S i) (TLRef n)) (lift_lref_ge n (S h) (S i) 
-H0)))))))) (\lambda (k: K).(\lambda (t: T).(\lambda (H: ((\forall (i: 
+(lift (S h) (S i) (TLRef n)) (lift_lref_lt n (S h) (S i) (le_S_n (S n) (S i) 
+(le_S (S (S n)) (S i) (le_n_S (S n) i H0)))))) (\lambda (H0: (eq nat n 
+i)).(let H1 \def (eq_ind_r nat i (\lambda (n0: nat).(le h n0)) H n H0) in 
+(eq_ind nat n (\lambda (n0: nat).(subst1 n0 (TLRef h) (lift (S h) (S n0) 
+(TLRef n)) (lift (S h) n0 (TLRef n)))) (eq_ind_r T (TLRef n) (\lambda (t: 
+T).(subst1 n (TLRef h) t (lift (S h) n (TLRef n)))) (eq_ind_r T (TLRef (plus 
+n (S h))) (\lambda (t: T).(subst1 n (TLRef h) (TLRef n) t)) (eq_ind nat (S 
+(plus n h)) (\lambda (n0: nat).(subst1 n (TLRef h) (TLRef n) (TLRef n0))) 
+(eq_ind_r nat (plus h n) (\lambda (n0: nat).(subst1 n (TLRef h) (TLRef n) 
+(TLRef (S n0)))) (eq_ind nat (plus h (S n)) (\lambda (n0: nat).(subst1 n 
+(TLRef h) (TLRef n) (TLRef n0))) (eq_ind T (lift (S n) O (TLRef h)) (\lambda 
+(t: T).(subst1 n (TLRef h) (TLRef n) t)) (subst1_single n (TLRef h) (TLRef n) 
+(lift (S n) O (TLRef h)) (subst0_lref (TLRef h) n)) (TLRef (plus h (S n))) 
+(lift_lref_ge h (S n) O (le_O_n h))) (S (plus h n)) (sym_eq nat (S (plus h 
+n)) (plus h (S n)) (plus_n_Sm h n))) (plus n h) (plus_sym n h)) (plus n (S 
+h)) (plus_n_Sm n h)) (lift (S h) n (TLRef n)) (lift_lref_ge n (S h) n (le_n 
+n))) (lift (S h) (S n) (TLRef n)) (lift_lref_lt n (S h) (S n) (le_n (S n)))) 
+i H0))) (\lambda (H0: (lt i n)).(eq_ind_r T (TLRef (plus n (S h))) (\lambda 
+(t: T).(subst1 i (TLRef h) t (lift (S h) i (TLRef n)))) (eq_ind_r T (TLRef 
+(plus n (S h))) (\lambda (t: T).(subst1 i (TLRef h) (TLRef (plus n (S h))) 
+t)) (subst1_refl i (TLRef h) (TLRef (plus n (S h)))) (lift (S h) i (TLRef n)) 
+(lift_lref_ge n (S h) i (le_S_n i n (le_S_n (S i) (S n) (le_S (S (S i)) (S n) 
+(le_n_S (S i) n H0)))))) (lift (S h) (S i) (TLRef n)) (lift_lref_ge n (S h) 
+(S i) H0)))))))) (\lambda (k: K).(\lambda (t: T).(\lambda (H: ((\forall (i: 
 nat).(\forall (h: nat).((le h i) \to (subst1 i (TLRef h) (lift (S h) (S i) t) 
 (lift (S h) i t))))))).(\lambda (t0: T).(\lambda (H0: ((\forall (i: 
 nat).(\forall (h: nat).((le h i) \to (subst1 i (TLRef h) (lift (S h) (S i) 
@@ -173,7 +162,4 @@ h H1) k (lift (S h) (s k (S i)) t0) (lift (S h) (s k i) t0) (eq_ind_r nat (S
 (S h) (s k i) t0))) (H0 (s k i) h (le_trans h i (s k i) H1 (s_inc k i))) (s k 
 (S i)) (s_S k i))) (lift (S h) i (THead k t t0)) (lift_head k t t0 (S h) i)) 
 (lift (S h) (S i) (THead k t t0)) (lift_head k t t0 (S h) (S i))))))))))) u).
-(* COMMENTS
-Initial nodes: 1421
-END *)