X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Fiso%2Ffwd.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Fiso%2Ffwd.ma;h=9402e8cbfc01e0e79a8ca48c749a24e2a86c6d02;hb=31d27ada1bbad75aa0c44cd3e079cc4eba17d27e;hp=038a53cf874c4d592a770570a1467c5afab17bfd;hpb=ac6c6c1f9934fefb4e462f3aa3e1429460703037;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd.ma
index 038a53cf8..9402e8cbf 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd.ma
@@ -201,3 +201,111 @@ H9))) t3 (sym_eq T t3 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)) H7))) v1
 (refl_equal T (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 
 t2)))) (refl_equal T (THead (Bind b) v t))))))))) vs)))))))).
 
+theorem iso_gen_sort:
+ \forall (u2: T).(\forall (n1: nat).((iso (TSort n1) u2) \to (ex nat (\lambda 
+(n2: nat).(eq T u2 (TSort n2))))))
+\def
+ \lambda (u2: T).(\lambda (n1: nat).(\lambda (H: (iso (TSort n1) u2)).(let H0 
+\def (match H in iso return (\lambda (t: T).(\lambda (t0: T).(\lambda (_: 
+(iso t t0)).((eq T t (TSort n1)) \to ((eq T t0 u2) \to (ex nat (\lambda (n2: 
+nat).(eq T u2 (TSort n2))))))))) with [(iso_sort n0 n2) \Rightarrow (\lambda 
+(H0: (eq T (TSort n0) (TSort n1))).(\lambda (H1: (eq T (TSort n2) u2)).((let 
+H2 \def (f_equal T nat (\lambda (e: T).(match e in T return (\lambda (_: 
+T).nat) with [(TSort n) \Rightarrow n | (TLRef _) \Rightarrow n0 | (THead _ _ 
+_) \Rightarrow n0])) (TSort n0) (TSort n1) H0) in (eq_ind nat n1 (\lambda (_: 
+nat).((eq T (TSort n2) u2) \to (ex nat (\lambda (n3: nat).(eq T u2 (TSort 
+n3)))))) (\lambda (H3: (eq T (TSort n2) u2)).(eq_ind T (TSort n2) (\lambda 
+(t: T).(ex nat (\lambda (n3: nat).(eq T t (TSort n3))))) (ex_intro nat 
+(\lambda (n3: nat).(eq T (TSort n2) (TSort n3))) n2 (refl_equal T (TSort 
+n2))) u2 H3)) n0 (sym_eq nat n0 n1 H2))) H1))) | (iso_lref i1 i2) \Rightarrow 
+(\lambda (H0: (eq T (TLRef i1) (TSort n1))).(\lambda (H1: (eq T (TLRef i2) 
+u2)).((let H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T return 
+(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
+\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n1) H0) in 
+(False_ind ((eq T (TLRef i2) u2) \to (ex nat (\lambda (n2: nat).(eq T u2 
+(TSort n2))))) H2)) H1))) | (iso_head v1 v2 t1 t2 k) \Rightarrow (\lambda 
+(H0: (eq T (THead k v1 t1) (TSort n1))).(\lambda (H1: (eq T (THead k v2 t2) 
+u2)).((let H2 \def (eq_ind T (THead k v1 t1) (\lambda (e: T).(match e in T 
+return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
+\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n1) H0) in 
+(False_ind ((eq T (THead k v2 t2) u2) \to (ex nat (\lambda (n2: nat).(eq T u2 
+(TSort n2))))) H2)) H1)))]) in (H0 (refl_equal T (TSort n1)) (refl_equal T 
+u2))))).
+
+theorem iso_gen_lref:
+ \forall (u2: T).(\forall (n1: nat).((iso (TLRef n1) u2) \to (ex nat (\lambda 
+(n2: nat).(eq T u2 (TLRef n2))))))
+\def
+ \lambda (u2: T).(\lambda (n1: nat).(\lambda (H: (iso (TLRef n1) u2)).(let H0 
+\def (match H in iso return (\lambda (t: T).(\lambda (t0: T).(\lambda (_: 
+(iso t t0)).((eq T t (TLRef n1)) \to ((eq T t0 u2) \to (ex nat (\lambda (n2: 
+nat).(eq T u2 (TLRef n2))))))))) with [(iso_sort n0 n2) \Rightarrow (\lambda 
+(H0: (eq T (TSort n0) (TLRef n1))).(\lambda (H1: (eq T (TSort n2) u2)).((let 
+H2 \def (eq_ind T (TSort n0) (\lambda (e: T).(match e in T return (\lambda 
+(_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | 
+(THead _ _ _) \Rightarrow False])) I (TLRef n1) H0) in (False_ind ((eq T 
+(TSort n2) u2) \to (ex nat (\lambda (n3: nat).(eq T u2 (TLRef n3))))) H2)) 
+H1))) | (iso_lref i1 i2) \Rightarrow (\lambda (H0: (eq T (TLRef i1) (TLRef 
+n1))).(\lambda (H1: (eq T (TLRef i2) u2)).((let H2 \def (f_equal T nat 
+(\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _) 
+\Rightarrow i1 | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i1])) 
+(TLRef i1) (TLRef n1) H0) in (eq_ind nat n1 (\lambda (_: nat).((eq T (TLRef 
+i2) u2) \to (ex nat (\lambda (n2: nat).(eq T u2 (TLRef n2)))))) (\lambda (H3: 
+(eq T (TLRef i2) u2)).(eq_ind T (TLRef i2) (\lambda (t: T).(ex nat (\lambda 
+(n2: nat).(eq T t (TLRef n2))))) (ex_intro nat (\lambda (n2: nat).(eq T 
+(TLRef i2) (TLRef n2))) i2 (refl_equal T (TLRef i2))) u2 H3)) i1 (sym_eq nat 
+i1 n1 H2))) H1))) | (iso_head v1 v2 t1 t2 k) \Rightarrow (\lambda (H0: (eq T 
+(THead k v1 t1) (TLRef n1))).(\lambda (H1: (eq T (THead k v2 t2) u2)).((let 
+H2 \def (eq_ind T (THead k v1 t1) (\lambda (e: T).(match e in T return 
+(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
+\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n1) H0) in 
+(False_ind ((eq T (THead k v2 t2) u2) \to (ex nat (\lambda (n2: nat).(eq T u2 
+(TLRef n2))))) H2)) H1)))]) in (H0 (refl_equal T (TLRef n1)) (refl_equal T 
+u2))))).
+
+theorem iso_gen_head:
+ \forall (k: K).(\forall (v1: T).(\forall (t1: T).(\forall (u2: T).((iso 
+(THead k v1 t1) u2) \to (ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T u2 
+(THead k v2 t2)))))))))
+\def
+ \lambda (k: K).(\lambda (v1: T).(\lambda (t1: T).(\lambda (u2: T).(\lambda 
+(H: (iso (THead k v1 t1) u2)).(let H0 \def (match H in iso return (\lambda 
+(t: T).(\lambda (t0: T).(\lambda (_: (iso t t0)).((eq T t (THead k v1 t1)) 
+\to ((eq T t0 u2) \to (ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T u2 
+(THead k v2 t2)))))))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq 
+T (TSort n1) (THead k v1 t1))).(\lambda (H1: (eq T (TSort n2) u2)).((let H2 
+\def (eq_ind T (TSort n1) (\lambda (e: T).(match e in T return (\lambda (_: 
+T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | 
+(THead _ _ _) \Rightarrow False])) I (THead k v1 t1) H0) in (False_ind ((eq T 
+(TSort n2) u2) \to (ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T u2 
+(THead k v2 t2)))))) H2)) H1))) | (iso_lref i1 i2) \Rightarrow (\lambda (H0: 
+(eq T (TLRef i1) (THead k v1 t1))).(\lambda (H1: (eq T (TLRef i2) u2)).((let 
+H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T return (\lambda 
+(_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | 
+(THead _ _ _) \Rightarrow False])) I (THead k v1 t1) H0) in (False_ind ((eq T 
+(TLRef i2) u2) \to (ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T u2 
+(THead k v2 t2)))))) H2)) H1))) | (iso_head v0 v2 t0 t2 k0) \Rightarrow 
+(\lambda (H0: (eq T (THead k0 v0 t0) (THead k v1 t1))).(\lambda (H1: (eq T 
+(THead k0 v2 t2) u2)).((let H2 \def (f_equal T T (\lambda (e: T).(match e in 
+T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _) 
+\Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead k0 v0 t0) (THead k v1 
+t1) H0) in ((let H3 \def (f_equal T T (\lambda (e: T).(match e in T return 
+(\lambda (_: T).T) with [(TSort _) \Rightarrow v0 | (TLRef _) \Rightarrow v0 
+| (THead _ t _) \Rightarrow t])) (THead k0 v0 t0) (THead k v1 t1) H0) in 
+((let H4 \def (f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: 
+T).K) with [(TSort _) \Rightarrow k0 | (TLRef _) \Rightarrow k0 | (THead k1 _ 
+_) \Rightarrow k1])) (THead k0 v0 t0) (THead k v1 t1) H0) in (eq_ind K k 
+(\lambda (k1: K).((eq T v0 v1) \to ((eq T t0 t1) \to ((eq T (THead k1 v2 t2) 
+u2) \to (ex_2 T T (\lambda (v3: T).(\lambda (t3: T).(eq T u2 (THead k v3 
+t3))))))))) (\lambda (H5: (eq T v0 v1)).(eq_ind T v1 (\lambda (_: T).((eq T 
+t0 t1) \to ((eq T (THead k v2 t2) u2) \to (ex_2 T T (\lambda (v3: T).(\lambda 
+(t3: T).(eq T u2 (THead k v3 t3)))))))) (\lambda (H6: (eq T t0 t1)).(eq_ind T 
+t1 (\lambda (_: T).((eq T (THead k v2 t2) u2) \to (ex_2 T T (\lambda (v3: 
+T).(\lambda (t3: T).(eq T u2 (THead k v3 t3))))))) (\lambda (H7: (eq T (THead 
+k v2 t2) u2)).(eq_ind T (THead k v2 t2) (\lambda (t: T).(ex_2 T T (\lambda 
+(v3: T).(\lambda (t3: T).(eq T t (THead k v3 t3)))))) (ex_2_intro T T 
+(\lambda (v3: T).(\lambda (t3: T).(eq T (THead k v2 t2) (THead k v3 t3)))) v2 
+t2 (refl_equal T (THead k v2 t2))) u2 H7)) t0 (sym_eq T t0 t1 H6))) v0 
+(sym_eq T v0 v1 H5))) k0 (sym_eq K k0 k H4))) H3)) H2)) H1)))]) in (H0 
+(refl_equal T (THead k v1 t1)) (refl_equal T u2))))))).
+