X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fpr3%2Fiso.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fpr3%2Fiso.ma;h=c56ee4c23eac10c64120d730572720271dbc7217;hb=8de8cf8adfa6fcda91047eb2c25535893ede046a;hp=7ff6beaf4bdbf370c98c1a976e2fab153717ea1c;hpb=d2caaf419cb6c92cb5ca8615f8eac4e12f3ab728;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/pr3/iso.ma b/matita/matita/contribs/lambdadelta/basic_1/pr3/iso.ma
index 7ff6beaf4..c56ee4c23 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/pr3/iso.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/pr3/iso.ma
@@ -20,7 +20,7 @@ include "basic_1/iso/props.ma".
 
 include "basic_1/tlist/fwd.ma".
 
-theorem pr3_iso_appls_abbr:
+lemma pr3_iso_appls_abbr:
  \forall (c: C).(\forall (d: C).(\forall (w: T).(\forall (i: nat).((getl i c 
 (CHead d (Bind Abbr) w)) \to (\forall (vs: TList).(let u1 \def (THeads (Flat 
 Appl) vs (TLRef i)) in (\forall (u2: T).((pr3 c u1 u2) \to ((((iso u1 u2) \to 
@@ -199,7 +199,7 @@ c x1 x5 H9 (Bind x0) (THead (Flat Appl) (lift (S O) O x4) x2) (THead (Flat
 Appl) (lift (S O) O x4) x3) (pr3_thin_dx (CHead c (Bind x0) x5) x2 x3 H10 
 (lift (S O) O x4) Appl)) u2 H7)))))))))))))) H4)) H3)))))))) vs)))))).
 
-theorem pr3_iso_appls_cast:
+lemma pr3_iso_appls_cast:
  \forall (c: C).(\forall (v: T).(\forall (t: T).(\forall (vs: TList).(let u1 
 \def (THeads (Flat Appl) vs (THead (Flat Cast) v t)) in (\forall (u2: 
 T).((pr3 c u1 u2) \to ((((iso u1 u2) \to (\forall (P: Prop).P))) \to (pr3 c 
@@ -359,7 +359,7 @@ O) O x4) x3)) (THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O x4) x2)) c
 (THead (Flat Appl) (lift (S O) O x4) x3) (pr3_thin_dx (CHead c (Bind x0) x5) 
 x2 x3 H9 (lift (S O) O x4) Appl)) u2 H6)))))))))))))) H3)) H2)))))))) vs)))).
 
-theorem pr3_iso_appl_bind:
+lemma pr3_iso_appl_bind:
  \forall (b: B).((not (eq B b Abst)) \to (\forall (v1: T).(\forall (v2: 
 T).(\forall (t: T).(let u1 \def (THead (Flat Appl) v1 (THead (Bind b) v2 t)) 
 in (\forall (c: C).(\forall (u2: T).((pr3 c u1 u2) \to ((((iso u1 u2) \to 
@@ -576,7 +576,7 @@ O) O x4) Appl))) (THead (Flat Appl) (lift (S O) O x4) (lift (S O) O (THead
 (Bind x0) x1 x2))) (lift_flat Appl x4 (THead (Bind x0) x1 x2) (S O) O)))) 
 H10))) u2 H6))))))))))))) H3)) H2)))))))))).
 
-theorem pr3_iso_appls_appl_bind:
+lemma pr3_iso_appls_appl_bind:
  \forall (b: B).((not (eq B b Abst)) \to (\forall (v: T).(\forall (u: 
 T).(\forall (t: T).(\forall (vs: TList).(let u1 \def (THeads (Flat Appl) vs 
 (THead (Flat Appl) v (THead (Bind b) u t))) in (\forall (c: C).(\forall (u2: 
@@ -744,7 +744,7 @@ Appl) (lift (S O) O x4) x2) (THead (Flat Appl) (lift (S O) O x4) x3)
 (pr3_thin_dx (CHead c (Bind x0) x5) x2 x3 H10 (lift (S O) O x4) Appl)) u2 
 H7)))))))))))))) H4)) H3))))))))) vs)))))).
 
-theorem pr3_iso_appls_bind:
+lemma pr3_iso_appls_bind:
  \forall (b: B).((not (eq B b Abst)) \to (\forall (vs: TList).(\forall (u: 
 T).(\forall (t: T).(let u1 \def (THeads (Flat Appl) vs (THead (Bind b) u t)) 
 in (\forall (c: C).(\forall (u2: T).((pr3 c u1 u2) \to ((((iso u1 u2) \to 
@@ -824,7 +824,7 @@ t) t0))) (iso_head t1 t1 (THeads (Flat Appl) ts0 (THead (Flat Appl) t (THead
 Appl) (lift (S O) O t) t0 (lifts (S O) O ts))) (lifts (S O) O (TApp ts t)) 
 (lifts_tapp (S O) O t ts))))))))))) vs))).
 
-theorem pr3_iso_beta:
+lemma pr3_iso_beta:
  \forall (v: T).(\forall (w: T).(\forall (t: T).(let u1 \def (THead (Flat 
 Appl) v (THead (Bind Abst) w t)) in (\forall (c: C).(\forall (u2: T).((pr3 c 
 u1 u2) \to ((((iso u1 u2) \to (\forall (P: Prop).P))) \to (pr3 c (THead (Bind 
@@ -962,7 +962,7 @@ Abst))) H3 Abst H17) in (let H23 \def (match (H22 (refl_equal B Abst)) in
 False with []) in H23))))))))) H14)) H13))))))) H9)))))))))))))) H2)) 
 H1)))))))).
 
-theorem pr3_iso_appls_beta:
+lemma pr3_iso_appls_beta:
  \forall (us: TList).(\forall (v: T).(\forall (w: T).(\forall (t: T).(let u1 
 \def (THeads (Flat Appl) us (THead (Flat Appl) v (THead (Bind Abst) w t))) in 
 (\forall (c: C).(\forall (u2: T).((pr3 c u1 u2) \to ((((iso u1 u2) \to