]> matita.cs.unibo.it Git - helm.git/commitdiff
some theorems about getl
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 6 Sep 2006 16:49:52 +0000 (16:49 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 6 Sep 2006 16:49:52 +0000 (16:49 +0000)
15 files changed:
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cimp/defs.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/defs.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/drop.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/fwd.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/props.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clen/getl.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/clear.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/dec.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/defs.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/drop.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/flt.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/fwd.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/props.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma

index 4e37576d20ca04a51569ea5255cd539a6027db58..98d1c163b6ed6261e92ef6fdb2fcd0f031bd17e3 100644 (file)
@@ -136,6 +136,7 @@ alias id "lt_n_Sn" = "cic:/Coq/Arith/Lt/lt_n_Sn.con".
 alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con".
 alias id "lt_wf_ind" = "cic:/Coq/Arith/Wf_nat/lt_wf_ind.con".
 alias id "bool_ind" = "cic:/Coq/Init/Datatypes/bool_ind.con".
+alias id "ex_ind" = "cic:/Coq/Init/Logic/ex_ind.con".
 
 theorem f_equal: \forall A,B:Type. \forall f:A \to B.
                  \forall x,y:A. x = y \to f x = f y.
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cimp/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cimp/defs.ma
new file mode 100644 (file)
index 0000000..84e8f45
--- /dev/null
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/cimp/defs".
+
+include "getl/defs.ma".
+
+definition cimp:
+ C \to (C \to Prop)
+\def
+ \lambda (c1: C).(\lambda (c2: C).(\forall (b: B).(\forall (d1: C).(\forall 
+(w: T).(\forall (h: nat).((getl h c1 (CHead d1 (Bind b) w)) \to (ex C 
+(\lambda (d2: C).(getl h c2 (CHead d2 (Bind b) w)))))))))).
+
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/defs.ma
new file mode 100644 (file)
index 0000000..3853cba
--- /dev/null
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/clear/defs".
+
+include "C/defs.ma".
+
+inductive clear: C \to (C \to Prop) \def
+| clear_bind: \forall (b: B).(\forall (e: C).(\forall (u: T).(clear (CHead e 
+(Bind b) u) (CHead e (Bind b) u))))
+| clear_flat: \forall (e: C).(\forall (c: C).((clear e c) \to (\forall (f: 
+F).(\forall (u: T).(clear (CHead e (Flat f) u) c))))).
+
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/drop.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/drop.ma
new file mode 100644 (file)
index 0000000..d30e4db
--- /dev/null
@@ -0,0 +1,175 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/clear/drop".
+
+include "clear/fwd.ma".
+
+include "drop/fwd.ma".
+
+theorem drop_clear:
+ \forall (c1: C).(\forall (c2: C).(\forall (i: nat).((drop (S i) O c1 c2) \to 
+(ex2_3 B C T (\lambda (b: B).(\lambda (e: C).(\lambda (v: T).(clear c1 (CHead 
+e (Bind b) v))))) (\lambda (_: B).(\lambda (e: C).(\lambda (_: T).(drop i O e 
+c2))))))))
+\def
+ \lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2: C).(\forall (i: 
+nat).((drop (S i) O c c2) \to (ex2_3 B C T (\lambda (b: B).(\lambda (e: 
+C).(\lambda (v: T).(clear c (CHead e (Bind b) v))))) (\lambda (_: B).(\lambda 
+(e: C).(\lambda (_: T).(drop i O e c2))))))))) (\lambda (n: nat).(\lambda 
+(c2: C).(\lambda (i: nat).(\lambda (H: (drop (S i) O (CSort n) c2)).(and3_ind 
+(eq C c2 (CSort n)) (eq nat (S i) O) (eq nat O O) (ex2_3 B C T (\lambda (b: 
+B).(\lambda (e: C).(\lambda (v: T).(clear (CSort n) (CHead e (Bind b) v))))) 
+(\lambda (_: B).(\lambda (e: C).(\lambda (_: T).(drop i O e c2))))) (\lambda 
+(_: (eq C c2 (CSort n))).(\lambda (H1: (eq nat (S i) O)).(\lambda (_: (eq nat 
+O O)).(let H3 \def (eq_ind nat (S i) (\lambda (ee: nat).(match ee in nat 
+return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow 
+True])) I O H1) in (False_ind (ex2_3 B C T (\lambda (b: B).(\lambda (e: 
+C).(\lambda (v: T).(clear (CSort n) (CHead e (Bind b) v))))) (\lambda (_: 
+B).(\lambda (e: C).(\lambda (_: T).(drop i O e c2))))) H3))))) (drop_gen_sort 
+n (S i) O c2 H)))))) (\lambda (c: C).(\lambda (H: ((\forall (c2: C).(\forall 
+(i: nat).((drop (S i) O c c2) \to (ex2_3 B C T (\lambda (b: B).(\lambda (e: 
+C).(\lambda (v: T).(clear c (CHead e (Bind b) v))))) (\lambda (_: B).(\lambda 
+(e: C).(\lambda (_: T).(drop i O e c2)))))))))).(\lambda (k: K).(\lambda (t: 
+T).(\lambda (c2: C).(\lambda (i: nat).(\lambda (H0: (drop (S i) O (CHead c k 
+t) c2)).((match k in K return (\lambda (k0: K).((drop (r k0 i) O c c2) \to 
+(ex2_3 B C T (\lambda (b: B).(\lambda (e: C).(\lambda (v: T).(clear (CHead c 
+k0 t) (CHead e (Bind b) v))))) (\lambda (_: B).(\lambda (e: C).(\lambda (_: 
+T).(drop i O e c2))))))) with [(Bind b) \Rightarrow (\lambda (H1: (drop (r 
+(Bind b) i) O c c2)).(ex2_3_intro B C T (\lambda (b0: B).(\lambda (e: 
+C).(\lambda (v: T).(clear (CHead c (Bind b) t) (CHead e (Bind b0) v))))) 
+(\lambda (_: B).(\lambda (e: C).(\lambda (_: T).(drop i O e c2)))) b c t 
+(clear_bind b c t) H1)) | (Flat f) \Rightarrow (\lambda (H1: (drop (r (Flat 
+f) i) O c c2)).(let H2 \def (H c2 i H1) in (ex2_3_ind B C T (\lambda (b: 
+B).(\lambda (e: C).(\lambda (v: T).(clear c (CHead e (Bind b) v))))) (\lambda 
+(_: B).(\lambda (e: C).(\lambda (_: T).(drop i O e c2)))) (ex2_3 B C T 
+(\lambda (b: B).(\lambda (e: C).(\lambda (v: T).(clear (CHead c (Flat f) t) 
+(CHead e (Bind b) v))))) (\lambda (_: B).(\lambda (e: C).(\lambda (_: 
+T).(drop i O e c2))))) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: 
+T).(\lambda (H3: (clear c (CHead x1 (Bind x0) x2))).(\lambda (H4: (drop i O 
+x1 c2)).(ex2_3_intro B C T (\lambda (b: B).(\lambda (e: C).(\lambda (v: 
+T).(clear (CHead c (Flat f) t) (CHead e (Bind b) v))))) (\lambda (_: 
+B).(\lambda (e: C).(\lambda (_: T).(drop i O e c2)))) x0 x1 x2 (clear_flat c 
+(CHead x1 (Bind x0) x2) H3 f t) H4)))))) H2)))]) (drop_gen_drop k c c2 t i 
+H0))))))))) c1).
+
+theorem drop_clear_O:
+ \forall (b: B).(\forall (c: C).(\forall (e1: C).(\forall (u: T).((clear c 
+(CHead e1 (Bind b) u)) \to (\forall (e2: C).(\forall (i: nat).((drop i O e1 
+e2) \to (drop (S i) O c e2))))))))
+\def
+ \lambda (b: B).(\lambda (c: C).(C_ind (\lambda (c0: C).(\forall (e1: 
+C).(\forall (u: T).((clear c0 (CHead e1 (Bind b) u)) \to (\forall (e2: 
+C).(\forall (i: nat).((drop i O e1 e2) \to (drop (S i) O c0 e2)))))))) 
+(\lambda (n: nat).(\lambda (e1: C).(\lambda (u: T).(\lambda (H: (clear (CSort 
+n) (CHead e1 (Bind b) u))).(\lambda (e2: C).(\lambda (i: nat).(\lambda (_: 
+(drop i O e1 e2)).(clear_gen_sort (CHead e1 (Bind b) u) n H (drop (S i) O 
+(CSort n) e2))))))))) (\lambda (c0: C).(\lambda (H: ((\forall (e1: 
+C).(\forall (u: T).((clear c0 (CHead e1 (Bind b) u)) \to (\forall (e2: 
+C).(\forall (i: nat).((drop i O e1 e2) \to (drop (S i) O c0 
+e2))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (e1: C).(\lambda (u: 
+T).(\lambda (H0: (clear (CHead c0 k t) (CHead e1 (Bind b) u))).(\lambda (e2: 
+C).(\lambda (i: nat).(\lambda (H1: (drop i O e1 e2)).((match k in K return 
+(\lambda (k0: K).((clear (CHead c0 k0 t) (CHead e1 (Bind b) u)) \to (drop (S 
+i) O (CHead c0 k0 t) e2))) with [(Bind b0) \Rightarrow (\lambda (H2: (clear 
+(CHead c0 (Bind b0) t) (CHead e1 (Bind b) u))).(let H3 \def (f_equal C C 
+(\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) 
+\Rightarrow e1 | (CHead c _ _) \Rightarrow c])) (CHead e1 (Bind b) u) (CHead 
+c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e1 (Bind b) u) t H2)) in ((let 
+H4 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) 
+with [(CSort _) \Rightarrow b | (CHead _ k _) \Rightarrow (match k in K 
+return (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow 
+b])])) (CHead e1 (Bind b) u) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 
+(CHead e1 (Bind b) u) t H2)) in ((let H5 \def (f_equal C T (\lambda (e: 
+C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | 
+(CHead _ _ t) \Rightarrow t])) (CHead e1 (Bind b) u) (CHead c0 (Bind b0) t) 
+(clear_gen_bind b0 c0 (CHead e1 (Bind b) u) t H2)) in (\lambda (H6: (eq B b 
+b0)).(\lambda (H7: (eq C e1 c0)).(let H8 \def (eq_ind C e1 (\lambda (c: 
+C).(drop i O c e2)) H1 c0 H7) in (eq_ind B b (\lambda (b1: B).(drop (S i) O 
+(CHead c0 (Bind b1) t) e2)) (drop_drop (Bind b) i c0 e2 H8 t) b0 H6))))) H4)) 
+H3))) | (Flat f) \Rightarrow (\lambda (H2: (clear (CHead c0 (Flat f) t) 
+(CHead e1 (Bind b) u))).(drop_drop (Flat f) i c0 e2 (H e1 u (clear_gen_flat f 
+c0 (CHead e1 (Bind b) u) t H2) e2 i H1) t))]) H0))))))))))) c)).
+
+theorem drop_clear_S:
+ \forall (x2: C).(\forall (x1: C).(\forall (h: nat).(\forall (d: nat).((drop 
+h (S d) x1 x2) \to (\forall (b: B).(\forall (c2: C).(\forall (u: T).((clear 
+x2 (CHead c2 (Bind b) u)) \to (ex2 C (\lambda (c1: C).(clear x1 (CHead c1 
+(Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2)))))))))))
+\def
+ \lambda (x2: C).(C_ind (\lambda (c: C).(\forall (x1: C).(\forall (h: 
+nat).(\forall (d: nat).((drop h (S d) x1 c) \to (\forall (b: B).(\forall (c2: 
+C).(\forall (u: T).((clear c (CHead c2 (Bind b) u)) \to (ex2 C (\lambda (c1: 
+C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 
+c2)))))))))))) (\lambda (n: nat).(\lambda (x1: C).(\lambda (h: nat).(\lambda 
+(d: nat).(\lambda (_: (drop h (S d) x1 (CSort n))).(\lambda (b: B).(\lambda 
+(c2: C).(\lambda (u: T).(\lambda (H0: (clear (CSort n) (CHead c2 (Bind b) 
+u))).(clear_gen_sort (CHead c2 (Bind b) u) n H0 (ex2 C (\lambda (c1: 
+C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 
+c2))))))))))))) (\lambda (c: C).(\lambda (H: ((\forall (x1: C).(\forall (h: 
+nat).(\forall (d: nat).((drop h (S d) x1 c) \to (\forall (b: B).(\forall (c2: 
+C).(\forall (u: T).((clear c (CHead c2 (Bind b) u)) \to (ex2 C (\lambda (c1: 
+C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 
+c2))))))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (x1: C).(\lambda (h: 
+nat).(\lambda (d: nat).(\lambda (H0: (drop h (S d) x1 (CHead c k 
+t))).(\lambda (b: B).(\lambda (c2: C).(\lambda (u: T).(\lambda (H1: (clear 
+(CHead c k t) (CHead c2 (Bind b) u))).(ex2_ind C (\lambda (e: C).(eq C x1 
+(CHead e k (lift h (r k d) t)))) (\lambda (e: C).(drop h (r k d) e c)) (ex2 C 
+(\lambda (c1: C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: 
+C).(drop h d c1 c2))) (\lambda (x: C).(\lambda (H2: (eq C x1 (CHead x k (lift 
+h (r k d) t)))).(\lambda (H3: (drop h (r k d) x c)).(eq_ind_r C (CHead x k 
+(lift h (r k d) t)) (\lambda (c0: C).(ex2 C (\lambda (c1: C).(clear c0 (CHead 
+c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2)))) ((match k in 
+K return (\lambda (k0: K).((clear (CHead c k0 t) (CHead c2 (Bind b) u)) \to 
+((drop h (r k0 d) x c) \to (ex2 C (\lambda (c1: C).(clear (CHead x k0 (lift h 
+(r k0 d) t)) (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 
+c2)))))) with [(Bind b0) \Rightarrow (\lambda (H4: (clear (CHead c (Bind b0) 
+t) (CHead c2 (Bind b) u))).(\lambda (H5: (drop h (r (Bind b0) d) x c)).(let 
+H6 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) 
+with [(CSort _) \Rightarrow c2 | (CHead c _ _) \Rightarrow c])) (CHead c2 
+(Bind b) u) (CHead c (Bind b0) t) (clear_gen_bind b0 c (CHead c2 (Bind b) u) 
+t H4)) in ((let H7 \def (f_equal C B (\lambda (e: C).(match e in C return 
+(\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k _) \Rightarrow 
+(match k in K return (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat 
+_) \Rightarrow b])])) (CHead c2 (Bind b) u) (CHead c (Bind b0) t) 
+(clear_gen_bind b0 c (CHead c2 (Bind b) u) t H4)) in ((let H8 \def (f_equal C 
+T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _) 
+\Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead c2 (Bind b) u) (CHead c 
+(Bind b0) t) (clear_gen_bind b0 c (CHead c2 (Bind b) u) t H4)) in (\lambda 
+(H9: (eq B b b0)).(\lambda (H10: (eq C c2 c)).(eq_ind_r T t (\lambda (t0: 
+T).(ex2 C (\lambda (c1: C).(clear (CHead x (Bind b0) (lift h (r (Bind b0) d) 
+t)) (CHead c1 (Bind b) (lift h d t0)))) (\lambda (c1: C).(drop h d c1 c2)))) 
+(eq_ind_r C c (\lambda (c0: C).(ex2 C (\lambda (c1: C).(clear (CHead x (Bind 
+b0) (lift h (r (Bind b0) d) t)) (CHead c1 (Bind b) (lift h d t)))) (\lambda 
+(c1: C).(drop h d c1 c0)))) (eq_ind_r B b0 (\lambda (b1: B).(ex2 C (\lambda 
+(c1: C).(clear (CHead x (Bind b0) (lift h (r (Bind b0) d) t)) (CHead c1 (Bind 
+b1) (lift h d t)))) (\lambda (c1: C).(drop h d c1 c)))) (ex_intro2 C (\lambda 
+(c1: C).(clear (CHead x (Bind b0) (lift h (r (Bind b0) d) t)) (CHead c1 (Bind 
+b0) (lift h d t)))) (\lambda (c1: C).(drop h d c1 c)) x (clear_bind b0 x 
+(lift h d t)) H5) b H9) c2 H10) u H8)))) H7)) H6)))) | (Flat f) \Rightarrow 
+(\lambda (H4: (clear (CHead c (Flat f) t) (CHead c2 (Bind b) u))).(\lambda 
+(H5: (drop h (r (Flat f) d) x c)).(let H6 \def (H x h d H5 b c2 u 
+(clear_gen_flat f c (CHead c2 (Bind b) u) t H4)) in (ex2_ind C (\lambda (c1: 
+C).(clear x (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 
+c2)) (ex2 C (\lambda (c1: C).(clear (CHead x (Flat f) (lift h (r (Flat f) d) 
+t)) (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2))) 
+(\lambda (x0: C).(\lambda (H7: (clear x (CHead x0 (Bind b) (lift h d 
+u)))).(\lambda (H8: (drop h d x0 c2)).(ex_intro2 C (\lambda (c1: C).(clear 
+(CHead x (Flat f) (lift h (r (Flat f) d) t)) (CHead c1 (Bind b) (lift h d 
+u)))) (\lambda (c1: C).(drop h d c1 c2)) x0 (clear_flat x (CHead x0 (Bind b) 
+(lift h d u)) H7 f (lift h (r (Flat f) d) t)) H8)))) H6))))]) H1 H3) x1 
+H2)))) (drop_gen_skip_r c x1 t h d k H0)))))))))))))) x2).
+
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/fwd.ma
new file mode 100644 (file)
index 0000000..2c8a2c8
--- /dev/null
@@ -0,0 +1,159 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/clear/fwd".
+
+include "clear/defs.ma".
+
+theorem clear_gen_sort:
+ \forall (x: C).(\forall (n: nat).((clear (CSort n) x) \to (\forall (P: 
+Prop).P)))
+\def
+ \lambda (x: C).(\lambda (n: nat).(\lambda (H: (clear (CSort n) x)).(\lambda 
+(P: Prop).(let H0 \def (match H in clear return (\lambda (c: C).(\lambda (c0: 
+C).(\lambda (_: (clear c c0)).((eq C c (CSort n)) \to ((eq C c0 x) \to P))))) 
+with [(clear_bind b e u) \Rightarrow (\lambda (H0: (eq C (CHead e (Bind b) u) 
+(CSort n))).(\lambda (H1: (eq C (CHead e (Bind b) u) x)).((let H2 \def 
+(eq_ind C (CHead e (Bind b) u) (\lambda (e0: C).(match e0 in C return 
+(\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _) 
+\Rightarrow True])) I (CSort n) H0) in (False_ind ((eq C (CHead e (Bind b) u) 
+x) \to P) H2)) H1))) | (clear_flat e c H0 f u) \Rightarrow (\lambda (H1: (eq 
+C (CHead e (Flat f) u) (CSort n))).(\lambda (H2: (eq C c x)).((let H3 \def 
+(eq_ind C (CHead e (Flat f) u) (\lambda (e0: C).(match e0 in C return 
+(\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _) 
+\Rightarrow True])) I (CSort n) H1) in (False_ind ((eq C c x) \to ((clear e 
+c) \to P)) H3)) H2 H0)))]) in (H0 (refl_equal C (CSort n)) (refl_equal C 
+x)))))).
+
+theorem clear_gen_bind:
+ \forall (b: B).(\forall (e: C).(\forall (x: C).(\forall (u: T).((clear 
+(CHead e (Bind b) u) x) \to (eq C x (CHead e (Bind b) u))))))
+\def
+ \lambda (b: B).(\lambda (e: C).(\lambda (x: C).(\lambda (u: T).(\lambda (H: 
+(clear (CHead e (Bind b) u) x)).(let H0 \def (match H in clear return 
+(\lambda (c: C).(\lambda (c0: C).(\lambda (_: (clear c c0)).((eq C c (CHead e 
+(Bind b) u)) \to ((eq C c0 x) \to (eq C x (CHead e (Bind b) u))))))) with 
+[(clear_bind b0 e0 u0) \Rightarrow (\lambda (H0: (eq C (CHead e0 (Bind b0) 
+u0) (CHead e (Bind b) u))).(\lambda (H1: (eq C (CHead e0 (Bind b0) u0) 
+x)).((let H2 \def (f_equal C T (\lambda (e1: C).(match e1 in C return 
+(\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t) \Rightarrow 
+t])) (CHead e0 (Bind b0) u0) (CHead e (Bind b) u) H0) in ((let H3 \def 
+(f_equal C B (\lambda (e1: C).(match e1 in C return (\lambda (_: C).B) with 
+[(CSort _) \Rightarrow b0 | (CHead _ k _) \Rightarrow (match k in K return 
+(\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow 
+b0])])) (CHead e0 (Bind b0) u0) (CHead e (Bind b) u) H0) in ((let H4 \def 
+(f_equal C C (\lambda (e1: C).(match e1 in C return (\lambda (_: C).C) with 
+[(CSort _) \Rightarrow e0 | (CHead c _ _) \Rightarrow c])) (CHead e0 (Bind 
+b0) u0) (CHead e (Bind b) u) H0) in (eq_ind C e (\lambda (c: C).((eq B b0 b) 
+\to ((eq T u0 u) \to ((eq C (CHead c (Bind b0) u0) x) \to (eq C x (CHead e 
+(Bind b) u)))))) (\lambda (H5: (eq B b0 b)).(eq_ind B b (\lambda (b1: B).((eq 
+T u0 u) \to ((eq C (CHead e (Bind b1) u0) x) \to (eq C x (CHead e (Bind b) 
+u))))) (\lambda (H6: (eq T u0 u)).(eq_ind T u (\lambda (t: T).((eq C (CHead e 
+(Bind b) t) x) \to (eq C x (CHead e (Bind b) u)))) (\lambda (H7: (eq C (CHead 
+e (Bind b) u) x)).(eq_ind C (CHead e (Bind b) u) (\lambda (c: C).(eq C c 
+(CHead e (Bind b) u))) (refl_equal C (CHead e (Bind b) u)) x H7)) u0 (sym_eq 
+T u0 u H6))) b0 (sym_eq B b0 b H5))) e0 (sym_eq C e0 e H4))) H3)) H2)) H1))) 
+| (clear_flat e0 c H0 f u0) \Rightarrow (\lambda (H1: (eq C (CHead e0 (Flat 
+f) u0) (CHead e (Bind b) u))).(\lambda (H2: (eq C c x)).((let H3 \def (eq_ind 
+C (CHead e0 (Flat f) u0) (\lambda (e1: C).(match e1 in C return (\lambda (_: 
+C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match 
+k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat 
+_) \Rightarrow True])])) I (CHead e (Bind b) u) H1) in (False_ind ((eq C c x) 
+\to ((clear e0 c) \to (eq C x (CHead e (Bind b) u)))) H3)) H2 H0)))]) in (H0 
+(refl_equal C (CHead e (Bind b) u)) (refl_equal C x))))))).
+
+theorem clear_gen_flat:
+ \forall (f: F).(\forall (e: C).(\forall (x: C).(\forall (u: T).((clear 
+(CHead e (Flat f) u) x) \to (clear e x)))))
+\def
+ \lambda (f: F).(\lambda (e: C).(\lambda (x: C).(\lambda (u: T).(\lambda (H: 
+(clear (CHead e (Flat f) u) x)).(let H0 \def (match H in clear return 
+(\lambda (c: C).(\lambda (c0: C).(\lambda (_: (clear c c0)).((eq C c (CHead e 
+(Flat f) u)) \to ((eq C c0 x) \to (clear e x)))))) with [(clear_bind b e0 u0) 
+\Rightarrow (\lambda (H0: (eq C (CHead e0 (Bind b) u0) (CHead e (Flat f) 
+u))).(\lambda (H1: (eq C (CHead e0 (Bind b) u0) x)).((let H2 \def (eq_ind C 
+(CHead e0 (Bind b) u0) (\lambda (e1: C).(match e1 in C return (\lambda (_: 
+C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match 
+k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat 
+_) \Rightarrow False])])) I (CHead e (Flat f) u) H0) in (False_ind ((eq C 
+(CHead e0 (Bind b) u0) x) \to (clear e x)) H2)) H1))) | (clear_flat e0 c H0 
+f0 u0) \Rightarrow (\lambda (H1: (eq C (CHead e0 (Flat f0) u0) (CHead e (Flat 
+f) u))).(\lambda (H2: (eq C c x)).((let H3 \def (f_equal C T (\lambda (e1: 
+C).(match e1 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | 
+(CHead _ _ t) \Rightarrow t])) (CHead e0 (Flat f0) u0) (CHead e (Flat f) u) 
+H1) in ((let H4 \def (f_equal C F (\lambda (e1: C).(match e1 in C return 
+(\lambda (_: C).F) with [(CSort _) \Rightarrow f0 | (CHead _ k _) \Rightarrow 
+(match k in K return (\lambda (_: K).F) with [(Bind _) \Rightarrow f0 | (Flat 
+f) \Rightarrow f])])) (CHead e0 (Flat f0) u0) (CHead e (Flat f) u) H1) in 
+((let H5 \def (f_equal C C (\lambda (e1: C).(match e1 in C return (\lambda 
+(_: C).C) with [(CSort _) \Rightarrow e0 | (CHead c _ _) \Rightarrow c])) 
+(CHead e0 (Flat f0) u0) (CHead e (Flat f) u) H1) in (eq_ind C e (\lambda (c0: 
+C).((eq F f0 f) \to ((eq T u0 u) \to ((eq C c x) \to ((clear c0 c) \to (clear 
+e x)))))) (\lambda (H6: (eq F f0 f)).(eq_ind F f (\lambda (_: F).((eq T u0 u) 
+\to ((eq C c x) \to ((clear e c) \to (clear e x))))) (\lambda (H7: (eq T u0 
+u)).(eq_ind T u (\lambda (_: T).((eq C c x) \to ((clear e c) \to (clear e 
+x)))) (\lambda (H8: (eq C c x)).(eq_ind C x (\lambda (c0: C).((clear e c0) 
+\to (clear e x))) (\lambda (H9: (clear e x)).H9) c (sym_eq C c x H8))) u0 
+(sym_eq T u0 u H7))) f0 (sym_eq F f0 f H6))) e0 (sym_eq C e0 e H5))) H4)) 
+H3)) H2 H0)))]) in (H0 (refl_equal C (CHead e (Flat f) u)) (refl_equal C 
+x))))))).
+
+theorem clear_gen_flat_r:
+ \forall (f: F).(\forall (x: C).(\forall (e: C).(\forall (u: T).((clear x 
+(CHead e (Flat f) u)) \to (\forall (P: Prop).P)))))
+\def
+ \lambda (f: F).(\lambda (x: C).(\lambda (e: C).(\lambda (u: T).(\lambda (H: 
+(clear x (CHead e (Flat f) u))).(\lambda (P: Prop).(insert_eq C (CHead e 
+(Flat f) u) (\lambda (c: C).(clear x c)) P (\lambda (y: C).(\lambda (H0: 
+(clear x y)).(clear_ind (\lambda (_: C).(\lambda (c0: C).((eq C c0 (CHead e 
+(Flat f) u)) \to P))) (\lambda (b: B).(\lambda (e0: C).(\lambda (u0: 
+T).(\lambda (H1: (eq C (CHead e0 (Bind b) u0) (CHead e (Flat f) u))).(let H2 
+\def (eq_ind C (CHead e0 (Bind b) u0) (\lambda (ee: C).(match ee in C return 
+(\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) 
+\Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _) 
+\Rightarrow True | (Flat _) \Rightarrow False])])) I (CHead e (Flat f) u) H1) 
+in (False_ind P H2)))))) (\lambda (e0: C).(\lambda (c: C).(\lambda (H1: 
+(clear e0 c)).(\lambda (H2: (((eq C c (CHead e (Flat f) u)) \to P))).(\lambda 
+(_: F).(\lambda (_: T).(\lambda (H3: (eq C c (CHead e (Flat f) u))).(let H4 
+\def (eq_ind C c (\lambda (c: C).((eq C c (CHead e (Flat f) u)) \to P)) H2 
+(CHead e (Flat f) u) H3) in (let H5 \def (eq_ind C c (\lambda (c: C).(clear 
+e0 c)) H1 (CHead e (Flat f) u) H3) in (H4 (refl_equal C (CHead e (Flat f) 
+u)))))))))))) x y H0))) H)))))).
+
+theorem clear_gen_all:
+ \forall (c1: C).(\forall (c2: C).((clear c1 c2) \to (ex_3 B C T (\lambda (b: 
+B).(\lambda (e: C).(\lambda (u: T).(eq C c2 (CHead e (Bind b) u))))))))
+\def
+ \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (clear c1 c2)).(clear_ind 
+(\lambda (_: C).(\lambda (c0: C).(ex_3 B C T (\lambda (b: B).(\lambda (e: 
+C).(\lambda (u: T).(eq C c0 (CHead e (Bind b) u)))))))) (\lambda (b: 
+B).(\lambda (e: C).(\lambda (u: T).(ex_3_intro B C T (\lambda (b0: 
+B).(\lambda (e0: C).(\lambda (u0: T).(eq C (CHead e (Bind b) u) (CHead e0 
+(Bind b0) u0))))) b e u (refl_equal C (CHead e (Bind b) u)))))) (\lambda (e: 
+C).(\lambda (c: C).(\lambda (H0: (clear e c)).(\lambda (H1: (ex_3 B C T 
+(\lambda (b: B).(\lambda (e: C).(\lambda (u: T).(eq C c (CHead e (Bind b) 
+u))))))).(\lambda (_: F).(\lambda (_: T).(let H2 \def H1 in (ex_3_ind B C T 
+(\lambda (b: B).(\lambda (e0: C).(\lambda (u0: T).(eq C c (CHead e0 (Bind b) 
+u0))))) (ex_3 B C T (\lambda (b: B).(\lambda (e0: C).(\lambda (u0: T).(eq C c 
+(CHead e0 (Bind b) u0)))))) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: 
+T).(\lambda (H3: (eq C c (CHead x1 (Bind x0) x2))).(let H4 \def (eq_ind C c 
+(\lambda (c: C).(clear e c)) H0 (CHead x1 (Bind x0) x2) H3) in (eq_ind_r C 
+(CHead x1 (Bind x0) x2) (\lambda (c0: C).(ex_3 B C T (\lambda (b: B).(\lambda 
+(e0: C).(\lambda (u0: T).(eq C c0 (CHead e0 (Bind b) u0))))))) (ex_3_intro B 
+C T (\lambda (b: B).(\lambda (e0: C).(\lambda (u0: T).(eq C (CHead x1 (Bind 
+x0) x2) (CHead e0 (Bind b) u0))))) x0 x1 x2 (refl_equal C (CHead x1 (Bind x0) 
+x2))) c H3)))))) H2)))))))) c1 c2 H))).
+
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/props.ma
new file mode 100644 (file)
index 0000000..d6c1350
--- /dev/null
@@ -0,0 +1,144 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/clear/props".
+
+include "clear/fwd.ma".
+
+theorem clear_clear:
+ \forall (c1: C).(\forall (c2: C).((clear c1 c2) \to (clear c2 c2)))
+\def
+ \lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2: C).((clear c c2) \to 
+(clear c2 c2)))) (\lambda (n: nat).(\lambda (c2: C).(\lambda (H: (clear 
+(CSort n) c2)).(clear_gen_sort c2 n H (clear c2 c2))))) (\lambda (c: 
+C).(\lambda (H: ((\forall (c2: C).((clear c c2) \to (clear c2 
+c2))))).(\lambda (k: K).(\lambda (t: T).(\lambda (c2: C).(\lambda (H0: (clear 
+(CHead c k t) c2)).((match k in K return (\lambda (k0: K).((clear (CHead c k0 
+t) c2) \to (clear c2 c2))) with [(Bind b) \Rightarrow (\lambda (H1: (clear 
+(CHead c (Bind b) t) c2)).(eq_ind_r C (CHead c (Bind b) t) (\lambda (c0: 
+C).(clear c0 c0)) (clear_bind b c t) c2 (clear_gen_bind b c c2 t H1))) | 
+(Flat f) \Rightarrow (\lambda (H1: (clear (CHead c (Flat f) t) c2)).(H c2 
+(clear_gen_flat f c c2 t H1)))]) H0))))))) c1).
+
+theorem clear_mono:
+ \forall (c: C).(\forall (c1: C).((clear c c1) \to (\forall (c2: C).((clear c 
+c2) \to (eq C c1 c2)))))
+\def
+ \lambda (c: C).(C_ind (\lambda (c0: C).(\forall (c1: C).((clear c0 c1) \to 
+(\forall (c2: C).((clear c0 c2) \to (eq C c1 c2)))))) (\lambda (n: 
+nat).(\lambda (c1: C).(\lambda (_: (clear (CSort n) c1)).(\lambda (c2: 
+C).(\lambda (H0: (clear (CSort n) c2)).(clear_gen_sort c2 n H0 (eq C c1 
+c2))))))) (\lambda (c0: C).(\lambda (H: ((\forall (c1: C).((clear c0 c1) \to 
+(\forall (c2: C).((clear c0 c2) \to (eq C c1 c2))))))).(\lambda (k: 
+K).(\lambda (t: T).(\lambda (c1: C).(\lambda (H0: (clear (CHead c0 k t) 
+c1)).(\lambda (c2: C).(\lambda (H1: (clear (CHead c0 k t) c2)).((match k in K 
+return (\lambda (k0: K).((clear (CHead c0 k0 t) c1) \to ((clear (CHead c0 k0 
+t) c2) \to (eq C c1 c2)))) with [(Bind b) \Rightarrow (\lambda (H2: (clear 
+(CHead c0 (Bind b) t) c1)).(\lambda (H3: (clear (CHead c0 (Bind b) t) 
+c2)).(eq_ind_r C (CHead c0 (Bind b) t) (\lambda (c3: C).(eq C c1 c3)) 
+(eq_ind_r C (CHead c0 (Bind b) t) (\lambda (c3: C).(eq C c3 (CHead c0 (Bind 
+b) t))) (refl_equal C (CHead c0 (Bind b) t)) c1 (clear_gen_bind b c0 c1 t 
+H2)) c2 (clear_gen_bind b c0 c2 t H3)))) | (Flat f) \Rightarrow (\lambda (H2: 
+(clear (CHead c0 (Flat f) t) c1)).(\lambda (H3: (clear (CHead c0 (Flat f) t) 
+c2)).(H c1 (clear_gen_flat f c0 c1 t H2) c2 (clear_gen_flat f c0 c2 t 
+H3))))]) H0 H1))))))))) c).
+
+theorem clear_trans:
+ \forall (c1: C).(\forall (c: C).((clear c1 c) \to (\forall (c2: C).((clear c 
+c2) \to (clear c1 c2)))))
+\def
+ \lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c0: C).((clear c c0) \to 
+(\forall (c2: C).((clear c0 c2) \to (clear c c2)))))) (\lambda (n: 
+nat).(\lambda (c: C).(\lambda (H: (clear (CSort n) c)).(\lambda (c2: 
+C).(\lambda (_: (clear c c2)).(clear_gen_sort c n H (clear (CSort n) 
+c2))))))) (\lambda (c: C).(\lambda (H: ((\forall (c0: C).((clear c c0) \to 
+(\forall (c2: C).((clear c0 c2) \to (clear c c2))))))).(\lambda (k: 
+K).(\lambda (t: T).(\lambda (c0: C).(\lambda (H0: (clear (CHead c k t) 
+c0)).(\lambda (c2: C).(\lambda (H1: (clear c0 c2)).((match k in K return 
+(\lambda (k0: K).((clear (CHead c k0 t) c0) \to (clear (CHead c k0 t) c2))) 
+with [(Bind b) \Rightarrow (\lambda (H2: (clear (CHead c (Bind b) t) 
+c0)).(let H3 \def (eq_ind C c0 (\lambda (c: C).(clear c c2)) H1 (CHead c 
+(Bind b) t) (clear_gen_bind b c c0 t H2)) in (eq_ind_r C (CHead c (Bind b) t) 
+(\lambda (c3: C).(clear (CHead c (Bind b) t) c3)) (clear_bind b c t) c2 
+(clear_gen_bind b c c2 t H3)))) | (Flat f) \Rightarrow (\lambda (H2: (clear 
+(CHead c (Flat f) t) c0)).(clear_flat c c2 (H c0 (clear_gen_flat f c c0 t H2) 
+c2 H1) f t))]) H0))))))))) c1).
+
+theorem clear_ctail:
+ \forall (b: B).(\forall (c1: C).(\forall (c2: C).(\forall (u2: T).((clear c1 
+(CHead c2 (Bind b) u2)) \to (\forall (k: K).(\forall (u1: T).(clear (CTail k 
+u1 c1) (CHead (CTail k u1 c2) (Bind b) u2))))))))
+\def
+ \lambda (b: B).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2: 
+C).(\forall (u2: T).((clear c (CHead c2 (Bind b) u2)) \to (\forall (k: 
+K).(\forall (u1: T).(clear (CTail k u1 c) (CHead (CTail k u1 c2) (Bind b) 
+u2)))))))) (\lambda (n: nat).(\lambda (c2: C).(\lambda (u2: T).(\lambda (H: 
+(clear (CSort n) (CHead c2 (Bind b) u2))).(\lambda (k: K).(\lambda (u1: 
+T).(match k in K return (\lambda (k0: K).(clear (CHead (CSort n) k0 u1) 
+(CHead (CTail k0 u1 c2) (Bind b) u2))) with [(Bind b0) \Rightarrow 
+(clear_gen_sort (CHead c2 (Bind b) u2) n H (clear (CHead (CSort n) (Bind b0) 
+u1) (CHead (CTail (Bind b0) u1 c2) (Bind b) u2))) | (Flat f) \Rightarrow 
+(clear_gen_sort (CHead c2 (Bind b) u2) n H (clear (CHead (CSort n) (Flat f) 
+u1) (CHead (CTail (Flat f) u1 c2) (Bind b) u2)))]))))))) (\lambda (c: 
+C).(\lambda (H: ((\forall (c2: C).(\forall (u2: T).((clear c (CHead c2 (Bind 
+b) u2)) \to (\forall (k: K).(\forall (u1: T).(clear (CTail k u1 c) (CHead 
+(CTail k u1 c2) (Bind b) u2))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda 
+(c2: C).(\lambda (u2: T).(\lambda (H0: (clear (CHead c k t) (CHead c2 (Bind 
+b) u2))).(\lambda (k0: K).(\lambda (u1: T).((match k in K return (\lambda 
+(k1: K).((clear (CHead c k1 t) (CHead c2 (Bind b) u2)) \to (clear (CHead 
+(CTail k0 u1 c) k1 t) (CHead (CTail k0 u1 c2) (Bind b) u2)))) with [(Bind b0) 
+\Rightarrow (\lambda (H1: (clear (CHead c (Bind b0) t) (CHead c2 (Bind b) 
+u2))).(let H2 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda 
+(_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c _ _) \Rightarrow c])) 
+(CHead c2 (Bind b) u2) (CHead c (Bind b0) t) (clear_gen_bind b0 c (CHead c2 
+(Bind b) u2) t H1)) in ((let H3 \def (f_equal C B (\lambda (e: C).(match e in 
+C return (\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k _) 
+\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b) 
+\Rightarrow b | (Flat _) \Rightarrow b])])) (CHead c2 (Bind b) u2) (CHead c 
+(Bind b0) t) (clear_gen_bind b0 c (CHead c2 (Bind b) u2) t H1)) in ((let H4 
+\def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) 
+with [(CSort _) \Rightarrow u2 | (CHead _ _ t) \Rightarrow t])) (CHead c2 
+(Bind b) u2) (CHead c (Bind b0) t) (clear_gen_bind b0 c (CHead c2 (Bind b) 
+u2) t H1)) in (\lambda (H5: (eq B b b0)).(\lambda (H6: (eq C c2 c)).(eq_ind_r 
+T t (\lambda (t0: T).(clear (CHead (CTail k0 u1 c) (Bind b0) t) (CHead (CTail 
+k0 u1 c2) (Bind b) t0))) (eq_ind_r C c (\lambda (c0: C).(clear (CHead (CTail 
+k0 u1 c) (Bind b0) t) (CHead (CTail k0 u1 c0) (Bind b) t))) (eq_ind B b 
+(\lambda (b1: B).(clear (CHead (CTail k0 u1 c) (Bind b1) t) (CHead (CTail k0 
+u1 c) (Bind b) t))) (clear_bind b (CTail k0 u1 c) t) b0 H5) c2 H6) u2 H4)))) 
+H3)) H2))) | (Flat f) \Rightarrow (\lambda (H1: (clear (CHead c (Flat f) t) 
+(CHead c2 (Bind b) u2))).(clear_flat (CTail k0 u1 c) (CHead (CTail k0 u1 c2) 
+(Bind b) u2) (H c2 u2 (clear_gen_flat f c (CHead c2 (Bind b) u2) t H1) k0 u1) 
+f t))]) H0)))))))))) c1)).
+
+theorem clear_cle:
+ \forall (c1: C).(\forall (c2: C).((clear c1 c2) \to (cle c2 c1)))
+\def
+ \lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2: C).((clear c c2) \to 
+(le (cweight c2) (cweight c))))) (\lambda (n: nat).(\lambda (c2: C).(\lambda 
+(H: (clear (CSort n) c2)).(clear_gen_sort c2 n H (le (cweight c2) O))))) 
+(\lambda (c: C).(\lambda (H: ((\forall (c2: C).((clear c c2) \to (le (cweight 
+c2) (cweight c)))))).(\lambda (k: K).(\lambda (t: T).(\lambda (c2: 
+C).(\lambda (H0: (clear (CHead c k t) c2)).((match k in K return (\lambda 
+(k0: K).((clear (CHead c k0 t) c2) \to (le (cweight c2) (plus (cweight c) 
+(tweight t))))) with [(Bind b) \Rightarrow (\lambda (H1: (clear (CHead c 
+(Bind b) t) c2)).(eq_ind_r C (CHead c (Bind b) t) (\lambda (c0: C).(le 
+(cweight c0) (plus (cweight c) (tweight t)))) (le_n (plus (cweight c) 
+(tweight t))) c2 (clear_gen_bind b c c2 t H1))) | (Flat f) \Rightarrow 
+(\lambda (H1: (clear (CHead c (Flat f) t) c2)).(le_S_n (cweight c2) (plus 
+(cweight c) (tweight t)) (le_n_S (cweight c2) (plus (cweight c) (tweight t)) 
+(le_plus_trans (cweight c2) (cweight c) (tweight t) (H c2 (clear_gen_flat f c 
+c2 t H1))))))]) H0))))))) c1).
+
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clen/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clen/getl.ma
new file mode 100644 (file)
index 0000000..2e027fe
--- /dev/null
@@ -0,0 +1,326 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/clen/getl".
+
+include "clen/defs.ma".
+
+include "getl/props.ma".
+
+theorem getl_ctail_clen:
+ \forall (b: B).(\forall (t: T).(\forall (c: C).(ex nat (\lambda (n: 
+nat).(getl (clen c) (CTail (Bind b) t c) (CHead (CSort n) (Bind b) t))))))
+\def
+ \lambda (b: B).(\lambda (t: T).(\lambda (c: C).(C_ind (\lambda (c0: C).(ex 
+nat (\lambda (n: nat).(getl (clen c0) (CTail (Bind b) t c0) (CHead (CSort n) 
+(Bind b) t))))) (\lambda (n: nat).(ex_intro nat (\lambda (n0: nat).(getl O 
+(CHead (CSort n) (Bind b) t) (CHead (CSort n0) (Bind b) t))) n (getl_refl b 
+(CSort n) t))) (\lambda (c0: C).(\lambda (H: (ex nat (\lambda (n: nat).(getl 
+(clen c0) (CTail (Bind b) t c0) (CHead (CSort n) (Bind b) t))))).(\lambda (k: 
+K).(\lambda (t0: T).(let H0 \def H in (ex_ind nat (\lambda (n: nat).(getl 
+(clen c0) (CTail (Bind b) t c0) (CHead (CSort n) (Bind b) t))) (ex nat 
+(\lambda (n: nat).(getl (s k (clen c0)) (CHead (CTail (Bind b) t c0) k t0) 
+(CHead (CSort n) (Bind b) t)))) (\lambda (x: nat).(\lambda (H1: (getl (clen 
+c0) (CTail (Bind b) t c0) (CHead (CSort x) (Bind b) t))).(match k in K return 
+(\lambda (k0: K).(ex nat (\lambda (n: nat).(getl (s k0 (clen c0)) (CHead 
+(CTail (Bind b) t c0) k0 t0) (CHead (CSort n) (Bind b) t))))) with [(Bind b0) 
+\Rightarrow (ex_intro nat (\lambda (n: nat).(getl (S (clen c0)) (CHead (CTail 
+(Bind b) t c0) (Bind b0) t0) (CHead (CSort n) (Bind b) t))) x (getl_head 
+(Bind b0) (clen c0) (CTail (Bind b) t c0) (CHead (CSort x) (Bind b) t) H1 
+t0)) | (Flat f) \Rightarrow (ex_intro nat (\lambda (n: nat).(getl (clen c0) 
+(CHead (CTail (Bind b) t c0) (Flat f) t0) (CHead (CSort n) (Bind b) t))) x 
+(getl_flat (CTail (Bind b) t c0) (CHead (CSort x) (Bind b) t) (clen c0) H1 f 
+t0))]))) H0)))))) c))).
+
+theorem getl_gen_tail:
+ \forall (k: K).(\forall (b: B).(\forall (u1: T).(\forall (u2: T).(\forall 
+(c2: C).(\forall (c1: C).(\forall (i: nat).((getl i (CTail k u1 c1) (CHead c2 
+(Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) 
+(\lambda (e: C).(getl i c1 (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: 
+nat).(eq nat i (clen c1))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: 
+nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n))))))))))))
+\def
+ \lambda (k: K).(\lambda (b: B).(\lambda (u1: T).(\lambda (u2: T).(\lambda 
+(c2: C).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (i: nat).((getl i 
+(CTail k u1 c) (CHead c2 (Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C 
+c2 (CTail k u1 e))) (\lambda (e: C).(getl i c (CHead e (Bind b) u2)))) (ex4 
+nat (\lambda (_: nat).(eq nat i (clen c))) (\lambda (_: nat).(eq K k (Bind 
+b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort 
+n)))))))) (\lambda (n: nat).(\lambda (i: nat).(match i in nat return (\lambda 
+(n0: nat).((getl n0 (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)) \to (or 
+(ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl n0 
+(CSort n) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat n0 
+(clen (CSort n)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq 
+T u1 u2)) (\lambda (n1: nat).(eq C c2 (CSort n1))))))) with [O \Rightarrow 
+(\lambda (H: (getl O (CHead (CSort n) k u1) (CHead c2 (Bind b) u2))).((match 
+k in K return (\lambda (k0: K).((clear (CHead (CSort n) k0 u1) (CHead c2 
+(Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k0 u1 e))) 
+(\lambda (e: C).(getl O (CSort n) (CHead e (Bind b) u2)))) (ex4 nat (\lambda 
+(_: nat).(eq nat O O)) (\lambda (_: nat).(eq K k0 (Bind b))) (\lambda (_: 
+nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))))))) with [(Bind 
+b0) \Rightarrow (\lambda (H0: (clear (CHead (CSort n) (Bind b0) u1) (CHead c2 
+(Bind b) u2))).(let H1 \def (f_equal C C (\lambda (e: C).(match e in C return 
+(\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c _ _) \Rightarrow 
+c])) (CHead c2 (Bind b) u2) (CHead (CSort n) (Bind b0) u1) (clear_gen_bind b0 
+(CSort n) (CHead c2 (Bind b) u2) u1 H0)) in ((let H2 \def (f_equal C B 
+(\lambda (e: C).(match e in C return (\lambda (_: C).B) with [(CSort _) 
+\Rightarrow b | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: 
+K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow b])])) (CHead c2 
+(Bind b) u2) (CHead (CSort n) (Bind b0) u1) (clear_gen_bind b0 (CSort n) 
+(CHead c2 (Bind b) u2) u1 H0)) in ((let H3 \def (f_equal C T (\lambda (e: 
+C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u2 | 
+(CHead _ _ t) \Rightarrow t])) (CHead c2 (Bind b) u2) (CHead (CSort n) (Bind 
+b0) u1) (clear_gen_bind b0 (CSort n) (CHead c2 (Bind b) u2) u1 H0)) in 
+(\lambda (H4: (eq B b b0)).(\lambda (H5: (eq C c2 (CSort n))).(eq_ind_r C 
+(CSort n) (\lambda (c: C).(or (ex2 C (\lambda (e: C).(eq C c (CTail (Bind b0) 
+u1 e))) (\lambda (e: C).(getl O (CSort n) (CHead e (Bind b) u2)))) (ex4 nat 
+(\lambda (_: nat).(eq nat O O)) (\lambda (_: nat).(eq K (Bind b0) (Bind b))) 
+(\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c (CSort n0)))))) 
+(eq_ind_r T u1 (\lambda (t: T).(or (ex2 C (\lambda (e: C).(eq C (CSort n) 
+(CTail (Bind b0) u1 e))) (\lambda (e: C).(getl O (CSort n) (CHead e (Bind b) 
+t)))) (ex4 nat (\lambda (_: nat).(eq nat O O)) (\lambda (_: nat).(eq K (Bind 
+b0) (Bind b))) (\lambda (_: nat).(eq T u1 t)) (\lambda (n0: nat).(eq C (CSort 
+n) (CSort n0)))))) (eq_ind_r B b0 (\lambda (b1: B).(or (ex2 C (\lambda (e: 
+C).(eq C (CSort n) (CTail (Bind b0) u1 e))) (\lambda (e: C).(getl O (CSort n) 
+(CHead e (Bind b1) u1)))) (ex4 nat (\lambda (_: nat).(eq nat O O)) (\lambda 
+(_: nat).(eq K (Bind b0) (Bind b1))) (\lambda (_: nat).(eq T u1 u1)) (\lambda 
+(n0: nat).(eq C (CSort n) (CSort n0)))))) (or_intror (ex2 C (\lambda (e: 
+C).(eq C (CSort n) (CTail (Bind b0) u1 e))) (\lambda (e: C).(getl O (CSort n) 
+(CHead e (Bind b0) u1)))) (ex4 nat (\lambda (_: nat).(eq nat O O)) (\lambda 
+(_: nat).(eq K (Bind b0) (Bind b0))) (\lambda (_: nat).(eq T u1 u1)) (\lambda 
+(n0: nat).(eq C (CSort n) (CSort n0)))) (ex4_intro nat (\lambda (_: nat).(eq 
+nat O O)) (\lambda (_: nat).(eq K (Bind b0) (Bind b0))) (\lambda (_: nat).(eq 
+T u1 u1)) (\lambda (n0: nat).(eq C (CSort n) (CSort n0))) n (refl_equal nat 
+O) (refl_equal K (Bind b0)) (refl_equal T u1) (refl_equal C (CSort n)))) b 
+H4) u2 H3) c2 H5)))) H2)) H1))) | (Flat f) \Rightarrow (\lambda (H0: (clear 
+(CHead (CSort n) (Flat f) u1) (CHead c2 (Bind b) u2))).(clear_gen_sort (CHead 
+c2 (Bind b) u2) n (clear_gen_flat f (CSort n) (CHead c2 (Bind b) u2) u1 H0) 
+(or (ex2 C (\lambda (e: C).(eq C c2 (CTail (Flat f) u1 e))) (\lambda (e: 
+C).(getl O (CSort n) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq 
+nat O O)) (\lambda (_: nat).(eq K (Flat f) (Bind b))) (\lambda (_: nat).(eq T 
+u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0)))))))]) (getl_gen_O (CHead 
+(CSort n) k u1) (CHead c2 (Bind b) u2) H))) | (S n0) \Rightarrow (\lambda (H: 
+(getl (S n0) (CHead (CSort n) k u1) (CHead c2 (Bind b) u2))).(getl_gen_sort n 
+(r k n0) (CHead c2 (Bind b) u2) (getl_gen_S k (CSort n) (CHead c2 (Bind b) 
+u2) u1 n0 H) (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda 
+(e: C).(getl (S n0) (CSort n) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: 
+nat).(eq nat (S n0) O)) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: 
+nat).(eq T u1 u2)) (\lambda (n1: nat).(eq C c2 (CSort n1)))))))]))) (\lambda 
+(c: C).(\lambda (H: ((\forall (i: nat).((getl i (CTail k u1 c) (CHead c2 
+(Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) 
+(\lambda (e: C).(getl i c (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: 
+nat).(eq nat i (clen c))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: 
+nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n))))))))).(\lambda (k0: 
+K).(\lambda (t: T).(\lambda (i: nat).(match i in nat return (\lambda (n: 
+nat).((getl n (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)) \to (or 
+(ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl n 
+(CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat n 
+(clen (CHead c k0 t)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: 
+nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))))))) with [O 
+\Rightarrow (\lambda (H0: (getl O (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind 
+b) u2))).((match k0 in K return (\lambda (k1: K).((clear (CHead (CTail k u1 
+c) k1 t) (CHead c2 (Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c2 
+(CTail k u1 e))) (\lambda (e: C).(getl O (CHead c k1 t) (CHead e (Bind b) 
+u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s k1 (clen c)))) (\lambda (_: 
+nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq 
+C c2 (CSort n))))))) with [(Bind b0) \Rightarrow (\lambda (H1: (clear (CHead 
+(CTail k u1 c) (Bind b0) t) (CHead c2 (Bind b) u2))).(let H2 \def (f_equal C 
+C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) 
+\Rightarrow c2 | (CHead c _ _) \Rightarrow c])) (CHead c2 (Bind b) u2) (CHead 
+(CTail k u1 c) (Bind b0) t) (clear_gen_bind b0 (CTail k u1 c) (CHead c2 (Bind 
+b) u2) t H1)) in ((let H3 \def (f_equal C B (\lambda (e: C).(match e in C 
+return (\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k _) 
+\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b) 
+\Rightarrow b | (Flat _) \Rightarrow b])])) (CHead c2 (Bind b) u2) (CHead 
+(CTail k u1 c) (Bind b0) t) (clear_gen_bind b0 (CTail k u1 c) (CHead c2 (Bind 
+b) u2) t H1)) in ((let H4 \def (f_equal C T (\lambda (e: C).(match e in C 
+return (\lambda (_: C).T) with [(CSort _) \Rightarrow u2 | (CHead _ _ t) 
+\Rightarrow t])) (CHead c2 (Bind b) u2) (CHead (CTail k u1 c) (Bind b0) t) 
+(clear_gen_bind b0 (CTail k u1 c) (CHead c2 (Bind b) u2) t H1)) in (\lambda 
+(H5: (eq B b b0)).(\lambda (H6: (eq C c2 (CTail k u1 c))).(eq_ind T u2 
+(\lambda (t0: T).(or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) 
+(\lambda (e: C).(getl O (CHead c (Bind b0) t0) (CHead e (Bind b) u2)))) (ex4 
+nat (\lambda (_: nat).(eq nat O (s (Bind b0) (clen c)))) (\lambda (_: 
+nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq 
+C c2 (CSort n)))))) (eq_ind B b (\lambda (b1: B).(or (ex2 C (\lambda (e: 
+C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Bind b1) u2) 
+(CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Bind b1) 
+(clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 
+u2)) (\lambda (n: nat).(eq C c2 (CSort n)))))) (let H7 \def (eq_ind C c2 
+(\lambda (c0: C).(\forall (i: nat).((getl i (CTail k u1 c) (CHead c0 (Bind b) 
+u2)) \to (or (ex2 C (\lambda (e: C).(eq C c0 (CTail k u1 e))) (\lambda (e: 
+C).(getl i c (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat i 
+(clen c))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 
+u2)) (\lambda (n: nat).(eq C c0 (CSort n)))))))) H (CTail k u1 c) H6) in 
+(eq_ind_r C (CTail k u1 c) (\lambda (c0: C).(or (ex2 C (\lambda (e: C).(eq C 
+c0 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Bind b) u2) (CHead e 
+(Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Bind b) (clen c)))) 
+(\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda 
+(n: nat).(eq C c0 (CSort n)))))) (or_introl (ex2 C (\lambda (e: C).(eq C 
+(CTail k u1 c) (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Bind b) u2) 
+(CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Bind b) 
+(clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 
+u2)) (\lambda (n: nat).(eq C (CTail k u1 c) (CSort n)))) (ex_intro2 C 
+(\lambda (e: C).(eq C (CTail k u1 c) (CTail k u1 e))) (\lambda (e: C).(getl O 
+(CHead c (Bind b) u2) (CHead e (Bind b) u2))) c (refl_equal C (CTail k u1 c)) 
+(getl_refl b c u2))) c2 H6)) b0 H5) t H4)))) H3)) H2))) | (Flat f) 
+\Rightarrow (\lambda (H1: (clear (CHead (CTail k u1 c) (Flat f) t) (CHead c2 
+(Bind b) u2))).(let H2 \def (H O (getl_intro O (CTail k u1 c) (CHead c2 (Bind 
+b) u2) (CTail k u1 c) (drop_refl (CTail k u1 c)) (clear_gen_flat f (CTail k 
+u1 c) (CHead c2 (Bind b) u2) t H1))) in (or_ind (ex2 C (\lambda (e: C).(eq C 
+c2 (CTail k u1 e))) (\lambda (e: C).(getl O c (CHead e (Bind b) u2)))) (ex4 
+nat (\lambda (_: nat).(eq nat O (clen c))) (\lambda (_: nat).(eq K k (Bind 
+b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n)))) 
+(or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl O 
+(CHead c (Flat f) t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq 
+nat O (s (Flat f) (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda 
+(_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n))))) (\lambda (H3: 
+(ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl O c 
+(CHead e (Bind b) u2))))).(ex2_ind C (\lambda (e: C).(eq C c2 (CTail k u1 
+e))) (\lambda (e: C).(getl O c (CHead e (Bind b) u2))) (or (ex2 C (\lambda 
+(e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Flat f) t) 
+(CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Flat f) 
+(clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 
+u2)) (\lambda (n: nat).(eq C c2 (CSort n))))) (\lambda (x: C).(\lambda (H4: 
+(eq C c2 (CTail k u1 x))).(\lambda (H5: (getl O c (CHead x (Bind b) 
+u2))).(eq_ind_r C (CTail k u1 x) (\lambda (c0: C).(or (ex2 C (\lambda (e: 
+C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Flat f) t) 
+(CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Flat f) 
+(clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 
+u2)) (\lambda (n: nat).(eq C c0 (CSort n)))))) (or_introl (ex2 C (\lambda (e: 
+C).(eq C (CTail k u1 x) (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c 
+(Flat f) t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s 
+(Flat f) (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: 
+nat).(eq T u1 u2)) (\lambda (n: nat).(eq C (CTail k u1 x) (CSort n)))) 
+(ex_intro2 C (\lambda (e: C).(eq C (CTail k u1 x) (CTail k u1 e))) (\lambda 
+(e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) u2))) x (refl_equal C 
+(CTail k u1 x)) (getl_flat c (CHead x (Bind b) u2) O H5 f t))) c2 H4)))) H3)) 
+(\lambda (H3: (ex4 nat (\lambda (_: nat).(eq nat O (clen c))) (\lambda (_: 
+nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq 
+C c2 (CSort n))))).(ex4_ind nat (\lambda (_: nat).(eq nat O (clen c))) 
+(\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda 
+(n: nat).(eq C c2 (CSort n))) (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 
+e))) (\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)))) 
+(ex4 nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) (\lambda (_: 
+nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq 
+C c2 (CSort n))))) (\lambda (x0: nat).(\lambda (H4: (eq nat O (clen 
+c))).(\lambda (H5: (eq K k (Bind b))).(\lambda (H6: (eq T u1 u2)).(\lambda 
+(H7: (eq C c2 (CSort x0))).(eq_ind_r C (CSort x0) (\lambda (c0: C).(or (ex2 C 
+(\lambda (e: C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c 
+(Flat f) t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s 
+(Flat f) (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: 
+nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c0 (CSort n)))))) (eq_ind T u1 
+(\lambda (t0: T).(or (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail k u1 e))) 
+(\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) t0)))) (ex4 
+nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) (\lambda (_: nat).(eq 
+K k (Bind b))) (\lambda (_: nat).(eq T u1 t0)) (\lambda (n: nat).(eq C (CSort 
+x0) (CSort n)))))) (eq_ind_r K (Bind b) (\lambda (k1: K).(or (ex2 C (\lambda 
+(e: C).(eq C (CSort x0) (CTail k1 u1 e))) (\lambda (e: C).(getl O (CHead c 
+(Flat f) t) (CHead e (Bind b) u1)))) (ex4 nat (\lambda (_: nat).(eq nat O (s 
+(Flat f) (clen c)))) (\lambda (_: nat).(eq K k1 (Bind b))) (\lambda (_: 
+nat).(eq T u1 u1)) (\lambda (n: nat).(eq C (CSort x0) (CSort n)))))) 
+(or_intror (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail (Bind b) u1 e))) 
+(\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) u1)))) (ex4 
+nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) (\lambda (_: nat).(eq 
+K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n: nat).(eq C 
+(CSort x0) (CSort n)))) (ex4_intro nat (\lambda (_: nat).(eq nat O (s (Flat 
+f) (clen c)))) (\lambda (_: nat).(eq K (Bind b) (Bind b))) (\lambda (_: 
+nat).(eq T u1 u1)) (\lambda (n: nat).(eq C (CSort x0) (CSort n))) x0 H4 
+(refl_equal K (Bind b)) (refl_equal T u1) (refl_equal C (CSort x0)))) k H5) 
+u2 H6) c2 H7)))))) H3)) H2)))]) (getl_gen_O (CHead (CTail k u1 c) k0 t) 
+(CHead c2 (Bind b) u2) H0))) | (S n) \Rightarrow (\lambda (H0: (getl (S n) 
+(CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2))).(let H_x \def (H (r k0 
+n) (getl_gen_S k0 (CTail k u1 c) (CHead c2 (Bind b) u2) t n H0)) in (let H1 
+\def H_x in (or_ind (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda 
+(e: C).(getl (r k0 n) c (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: 
+nat).(eq nat (r k0 n) (clen c))) (\lambda (_: nat).(eq K k (Bind b))) 
+(\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0)))) (or 
+(ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (S n) 
+(CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S 
+n) (s k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: 
+nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))))) (\lambda (H2: 
+(ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (r k0 
+n) c (CHead e (Bind b) u2))))).(ex2_ind C (\lambda (e: C).(eq C c2 (CTail k 
+u1 e))) (\lambda (e: C).(getl (r k0 n) c (CHead e (Bind b) u2))) (or (ex2 C 
+(\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead 
+c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s 
+k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T 
+u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))))) (\lambda (x: C).(\lambda 
+(H3: (eq C c2 (CTail k u1 x))).(\lambda (H4: (getl (r k0 n) c (CHead x (Bind 
+b) u2))).(let H5 \def (eq_ind C c2 (\lambda (c0: C).(getl (r k0 n) (CTail k 
+u1 c) (CHead c0 (Bind b) u2))) (getl_gen_S k0 (CTail k u1 c) (CHead c2 (Bind 
+b) u2) t n H0) (CTail k u1 x) H3) in (eq_ind_r C (CTail k u1 x) (\lambda (c0: 
+C).(or (ex2 C (\lambda (e: C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl 
+(S n) (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq 
+nat (S n) (s k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: 
+nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c0 (CSort n0)))))) (or_introl 
+(ex2 C (\lambda (e: C).(eq C (CTail k u1 x) (CTail k u1 e))) (\lambda (e: 
+C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: 
+nat).(eq nat (S n) (s k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) 
+(\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C (CTail k u1 x) 
+(CSort n0)))) (ex_intro2 C (\lambda (e: C).(eq C (CTail k u1 x) (CTail k u1 
+e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) u2))) x 
+(refl_equal C (CTail k u1 x)) (getl_head k0 n c (CHead x (Bind b) u2) H4 t))) 
+c2 H3))))) H2)) (\lambda (H2: (ex4 nat (\lambda (_: nat).(eq nat (r k0 n) 
+(clen c))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 
+u2)) (\lambda (n: nat).(eq C c2 (CSort n))))).(ex4_ind nat (\lambda (_: 
+nat).(eq nat (r k0 n) (clen c))) (\lambda (_: nat).(eq K k (Bind b))) 
+(\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))) (or 
+(ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (S n) 
+(CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S 
+n) (s k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: 
+nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))))) (\lambda (x0: 
+nat).(\lambda (H3: (eq nat (r k0 n) (clen c))).(\lambda (H4: (eq K k (Bind 
+b))).(\lambda (H5: (eq T u1 u2)).(\lambda (H6: (eq C c2 (CSort x0))).(let H7 
+\def (eq_ind C c2 (\lambda (c0: C).(getl (r k0 n) (CTail k u1 c) (CHead c0 
+(Bind b) u2))) (getl_gen_S k0 (CTail k u1 c) (CHead c2 (Bind b) u2) t n H0) 
+(CSort x0) H6) in (eq_ind_r C (CSort x0) (\lambda (c0: C).(or (ex2 C (\lambda 
+(e: C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) 
+(CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s k0 (clen 
+c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) 
+(\lambda (n0: nat).(eq C c0 (CSort n0)))))) (let H8 \def (eq_ind_r T u2 
+(\lambda (t: T).(getl (r k0 n) (CTail k u1 c) (CHead (CSort x0) (Bind b) t))) 
+H7 u1 H5) in (eq_ind T u1 (\lambda (t0: T).(or (ex2 C (\lambda (e: C).(eq C 
+(CSort x0) (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead 
+e (Bind b) t0)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s k0 (clen c)))) 
+(\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 t0)) (\lambda 
+(n0: nat).(eq C (CSort x0) (CSort n0)))))) (let H9 \def (eq_ind K k (\lambda 
+(k: K).(getl (r k0 n) (CTail k u1 c) (CHead (CSort x0) (Bind b) u1))) H8 
+(Bind b) H4) in (eq_ind_r K (Bind b) (\lambda (k1: K).(or (ex2 C (\lambda (e: 
+C).(eq C (CSort x0) (CTail k1 u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 
+t) (CHead e (Bind b) u1)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s k0 
+(clen c)))) (\lambda (_: nat).(eq K k1 (Bind b))) (\lambda (_: nat).(eq T u1 
+u1)) (\lambda (n0: nat).(eq C (CSort x0) (CSort n0)))))) (eq_ind nat (r k0 n) 
+(\lambda (n0: nat).(or (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail (Bind 
+b) u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) 
+u1)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s k0 n0))) (\lambda (_: 
+nat).(eq K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n1: 
+nat).(eq C (CSort x0) (CSort n1)))))) (eq_ind_r nat (S n) (\lambda (n0: 
+nat).(or (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail (Bind b) u1 e))) 
+(\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)))) (ex4 nat 
+(\lambda (_: nat).(eq nat (S n) n0)) (\lambda (_: nat).(eq K (Bind b) (Bind 
+b))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n1: nat).(eq C (CSort x0) 
+(CSort n1)))))) (or_intror (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail 
+(Bind b) u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) 
+u1)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (S n))) (\lambda (_: nat).(eq 
+K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n0: nat).(eq 
+C (CSort x0) (CSort n0)))) (ex4_intro nat (\lambda (_: nat).(eq nat (S n) (S 
+n))) (\lambda (_: nat).(eq K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1 
+u1)) (\lambda (n0: nat).(eq C (CSort x0) (CSort n0))) x0 (refl_equal nat (S 
+n)) (refl_equal K (Bind b)) (refl_equal T u1) (refl_equal C (CSort x0)))) (s 
+k0 (r k0 n)) (s_r k0 n)) (clen c) H3) k H4)) u2 H5)) c2 H6))))))) H2)) 
+H1))))])))))) c1)))))).
+
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/clear.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/clear.ma
new file mode 100644 (file)
index 0000000..2329dd9
--- /dev/null
@@ -0,0 +1,109 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/getl/clear".
+
+include "getl/props.ma".
+
+include "clear/drop.ma".
+
+theorem clear_getl_trans:
+ \forall (i: nat).(\forall (c2: C).(\forall (c3: C).((getl i c2 c3) \to 
+(\forall (c1: C).((clear c1 c2) \to (getl i c1 c3))))))
+\def
+ \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c2: C).(\forall (c3: 
+C).((getl n c2 c3) \to (\forall (c1: C).((clear c1 c2) \to (getl n c1 
+c3))))))) (\lambda (c2: C).(\lambda (c3: C).(\lambda (H: (getl O c2 
+c3)).(\lambda (c1: C).(\lambda (H0: (clear c1 c2)).(getl_intro O c1 c3 c1 
+(drop_refl c1) (clear_trans c1 c2 H0 c3 (getl_gen_O c2 c3 H)))))))) (\lambda 
+(n: nat).(\lambda (_: ((\forall (c2: C).(\forall (c3: C).((getl n c2 c3) \to 
+(\forall (c1: C).((clear c1 c2) \to (getl n c1 c3)))))))).(\lambda (c2: 
+C).(C_ind (\lambda (c: C).(\forall (c3: C).((getl (S n) c c3) \to (\forall 
+(c1: C).((clear c1 c) \to (getl (S n) c1 c3)))))) (\lambda (n0: nat).(\lambda 
+(c3: C).(\lambda (H0: (getl (S n) (CSort n0) c3)).(\lambda (c1: C).(\lambda 
+(_: (clear c1 (CSort n0))).(getl_gen_sort n0 (S n) c3 H0 (getl (S n) c1 
+c3))))))) (\lambda (c: C).(\lambda (_: ((\forall (c3: C).((getl (S n) c c3) 
+\to (\forall (c1: C).((clear c1 c) \to (getl (S n) c1 c3))))))).(\lambda (k: 
+K).(\lambda (t: T).(\lambda (c3: C).(\lambda (H1: (getl (S n) (CHead c k t) 
+c3)).(\lambda (c1: C).(\lambda (H2: (clear c1 (CHead c k t))).((match k in K 
+return (\lambda (k0: K).((getl (S n) (CHead c k0 t) c3) \to ((clear c1 (CHead 
+c k0 t)) \to (getl (S n) c1 c3)))) with [(Bind b) \Rightarrow (\lambda (H3: 
+(getl (S n) (CHead c (Bind b) t) c3)).(\lambda (H4: (clear c1 (CHead c (Bind 
+b) t))).(let H5 \def (getl_gen_all c c3 (r (Bind b) n) (getl_gen_S (Bind b) c 
+c3 t n H3)) in (ex2_ind C (\lambda (e: C).(drop n O c e)) (\lambda (e: 
+C).(clear e c3)) (getl (S n) c1 c3) (\lambda (x: C).(\lambda (H6: (drop n O c 
+x)).(\lambda (H7: (clear x c3)).(getl_intro (S n) c1 c3 x (drop_clear_O b c1 
+c t H4 x n H6) H7)))) H5)))) | (Flat f) \Rightarrow (\lambda (_: (getl (S n) 
+(CHead c (Flat f) t) c3)).(\lambda (H4: (clear c1 (CHead c (Flat f) 
+t))).(clear_gen_flat_r f c1 c t H4 (getl (S n) c1 c3))))]) H1 H2))))))))) 
+c2)))) i).
+
+theorem getl_clear_trans:
+ \forall (i: nat).(\forall (c1: C).(\forall (c2: C).((getl i c1 c2) \to 
+(\forall (c3: C).((clear c2 c3) \to (getl i c1 c3))))))
+\def
+ \lambda (i: nat).(\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (getl i c1 
+c2)).(\lambda (c3: C).(\lambda (H0: (clear c2 c3)).(let H1 \def (getl_gen_all 
+c1 c2 i H) in (ex2_ind C (\lambda (e: C).(drop i O c1 e)) (\lambda (e: 
+C).(clear e c2)) (getl i c1 c3) (\lambda (x: C).(\lambda (H2: (drop i O c1 
+x)).(\lambda (H3: (clear x c2)).(let H4 \def (clear_gen_all x c2 H3) in 
+(ex_3_ind B C T (\lambda (b: B).(\lambda (e: C).(\lambda (u: T).(eq C c2 
+(CHead e (Bind b) u))))) (getl i c1 c3) (\lambda (x0: B).(\lambda (x1: 
+C).(\lambda (x2: T).(\lambda (H5: (eq C c2 (CHead x1 (Bind x0) x2))).(let H6 
+\def (eq_ind C c2 (\lambda (c: C).(clear x c)) H3 (CHead x1 (Bind x0) x2) H5) 
+in (let H7 \def (eq_ind C c2 (\lambda (c: C).(clear c c3)) H0 (CHead x1 (Bind 
+x0) x2) H5) in (eq_ind_r C (CHead x1 (Bind x0) x2) (\lambda (c: C).(getl i c1 
+c)) (getl_intro i c1 (CHead x1 (Bind x0) x2) x H2 H6) c3 (clear_gen_bind x0 
+x1 c3 x2 H7)))))))) H4))))) H1))))))).
+
+theorem getl_clear_bind:
+ \forall (b: B).(\forall (c: C).(\forall (e1: C).(\forall (v: T).((clear c 
+(CHead e1 (Bind b) v)) \to (\forall (e2: C).(\forall (n: nat).((getl n e1 e2) 
+\to (getl (S n) c e2))))))))
+\def
+ \lambda (b: B).(\lambda (c: C).(C_ind (\lambda (c0: C).(\forall (e1: 
+C).(\forall (v: T).((clear c0 (CHead e1 (Bind b) v)) \to (\forall (e2: 
+C).(\forall (n: nat).((getl n e1 e2) \to (getl (S n) c0 e2)))))))) (\lambda 
+(n: nat).(\lambda (e1: C).(\lambda (v: T).(\lambda (H: (clear (CSort n) 
+(CHead e1 (Bind b) v))).(\lambda (e2: C).(\lambda (n0: nat).(\lambda (_: 
+(getl n0 e1 e2)).(clear_gen_sort (CHead e1 (Bind b) v) n H (getl (S n0) 
+(CSort n) e2))))))))) (\lambda (c0: C).(\lambda (H: ((\forall (e1: 
+C).(\forall (v: T).((clear c0 (CHead e1 (Bind b) v)) \to (\forall (e2: 
+C).(\forall (n: nat).((getl n e1 e2) \to (getl (S n) c0 e2))))))))).(\lambda 
+(k: K).(\lambda (t: T).(\lambda (e1: C).(\lambda (v: T).(\lambda (H0: (clear 
+(CHead c0 k t) (CHead e1 (Bind b) v))).(\lambda (e2: C).(\lambda (n: 
+nat).(\lambda (H1: (getl n e1 e2)).((match k in K return (\lambda (k0: 
+K).((clear (CHead c0 k0 t) (CHead e1 (Bind b) v)) \to (getl (S n) (CHead c0 
+k0 t) e2))) with [(Bind b0) \Rightarrow (\lambda (H2: (clear (CHead c0 (Bind 
+b0) t) (CHead e1 (Bind b) v))).(let H3 \def (f_equal C C (\lambda (e: 
+C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow e1 | 
+(CHead c _ _) \Rightarrow c])) (CHead e1 (Bind b) v) (CHead c0 (Bind b0) t) 
+(clear_gen_bind b0 c0 (CHead e1 (Bind b) v) t H2)) in ((let H4 \def (f_equal 
+C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with [(CSort _) 
+\Rightarrow b | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: 
+K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow b])])) (CHead e1 
+(Bind b) v) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e1 (Bind b) 
+v) t H2)) in ((let H5 \def (f_equal C T (\lambda (e: C).(match e in C return 
+(\lambda (_: C).T) with [(CSort _) \Rightarrow v | (CHead _ _ t) \Rightarrow 
+t])) (CHead e1 (Bind b) v) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 
+(CHead e1 (Bind b) v) t H2)) in (\lambda (H6: (eq B b b0)).(\lambda (H7: (eq 
+C e1 c0)).(let H8 \def (eq_ind C e1 (\lambda (c: C).(getl n c e2)) H1 c0 H7) 
+in (eq_ind B b (\lambda (b1: B).(getl (S n) (CHead c0 (Bind b1) t) e2)) 
+(getl_head (Bind b) n c0 e2 H8 t) b0 H6))))) H4)) H3))) | (Flat f) 
+\Rightarrow (\lambda (H2: (clear (CHead c0 (Flat f) t) (CHead e1 (Bind b) 
+v))).(getl_flat c0 e2 (S n) (H e1 v (clear_gen_flat f c0 (CHead e1 (Bind b) 
+v) t H2) e2 n H1) f t))]) H0))))))))))) c)).
+
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/dec.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/dec.ma
new file mode 100644 (file)
index 0000000..59c3775
--- /dev/null
@@ -0,0 +1,97 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/getl/dec".
+
+include "getl/props.ma".
+
+theorem getl_dec:
+ \forall (c: C).(\forall (i: nat).(or (ex_3 C B T (\lambda (e: C).(\lambda 
+(b: B).(\lambda (v: T).(getl i c (CHead e (Bind b) v)))))) (\forall (d: 
+C).((getl i c d) \to (\forall (P: Prop).P)))))
+\def
+ \lambda (c: C).(C_ind (\lambda (c0: C).(\forall (i: nat).(or (ex_3 C B T 
+(\lambda (e: C).(\lambda (b: B).(\lambda (v: T).(getl i c0 (CHead e (Bind b) 
+v)))))) (\forall (d: C).((getl i c0 d) \to (\forall (P: Prop).P)))))) 
+(\lambda (n: nat).(\lambda (i: nat).(or_intror (ex_3 C B T (\lambda (e: 
+C).(\lambda (b: B).(\lambda (v: T).(getl i (CSort n) (CHead e (Bind b) 
+v)))))) (\forall (d: C).((getl i (CSort n) d) \to (\forall (P: Prop).P))) 
+(\lambda (d: C).(\lambda (H: (getl i (CSort n) d)).(\lambda (P: 
+Prop).(getl_gen_sort n i d H P))))))) (\lambda (c0: C).(\lambda (H: ((\forall 
+(i: nat).(or (ex_3 C B T (\lambda (e: C).(\lambda (b: B).(\lambda (v: 
+T).(getl i c0 (CHead e (Bind b) v)))))) (\forall (d: C).((getl i c0 d) \to 
+(\forall (P: Prop).P))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (i: 
+nat).(match i in nat return (\lambda (n: nat).(or (ex_3 C B T (\lambda (e: 
+C).(\lambda (b: B).(\lambda (v: T).(getl n (CHead c0 k t) (CHead e (Bind b) 
+v)))))) (\forall (d: C).((getl n (CHead c0 k t) d) \to (\forall (P: 
+Prop).P))))) with [O \Rightarrow (match k in K return (\lambda (k0: K).(or 
+(ex_3 C B T (\lambda (e: C).(\lambda (b: B).(\lambda (v: T).(getl O (CHead c0 
+k0 t) (CHead e (Bind b) v)))))) (\forall (d: C).((getl O (CHead c0 k0 t) d) 
+\to (\forall (P: Prop).P))))) with [(Bind b) \Rightarrow (or_introl (ex_3 C B 
+T (\lambda (e: C).(\lambda (b0: B).(\lambda (v: T).(getl O (CHead c0 (Bind b) 
+t) (CHead e (Bind b0) v)))))) (\forall (d: C).((getl O (CHead c0 (Bind b) t) 
+d) \to (\forall (P: Prop).P))) (ex_3_intro C B T (\lambda (e: C).(\lambda 
+(b0: B).(\lambda (v: T).(getl O (CHead c0 (Bind b) t) (CHead e (Bind b0) 
+v))))) c0 b t (getl_refl b c0 t))) | (Flat f) \Rightarrow (let H_x \def (H O) 
+in (let H0 \def H_x in (or_ind (ex_3 C B T (\lambda (e: C).(\lambda (b: 
+B).(\lambda (v: T).(getl O c0 (CHead e (Bind b) v)))))) (\forall (d: 
+C).((getl O c0 d) \to (\forall (P: Prop).P))) (or (ex_3 C B T (\lambda (e: 
+C).(\lambda (b: B).(\lambda (v: T).(getl O (CHead c0 (Flat f) t) (CHead e 
+(Bind b) v)))))) (\forall (d: C).((getl O (CHead c0 (Flat f) t) d) \to 
+(\forall (P: Prop).P)))) (\lambda (H1: (ex_3 C B T (\lambda (e: C).(\lambda 
+(b: B).(\lambda (v: T).(getl O c0 (CHead e (Bind b) v))))))).(ex_3_ind C B T 
+(\lambda (e: C).(\lambda (b: B).(\lambda (v: T).(getl O c0 (CHead e (Bind b) 
+v))))) (or (ex_3 C B T (\lambda (e: C).(\lambda (b: B).(\lambda (v: T).(getl 
+O (CHead c0 (Flat f) t) (CHead e (Bind b) v)))))) (\forall (d: C).((getl O 
+(CHead c0 (Flat f) t) d) \to (\forall (P: Prop).P)))) (\lambda (x0: 
+C).(\lambda (x1: B).(\lambda (x2: T).(\lambda (H2: (getl O c0 (CHead x0 (Bind 
+x1) x2))).(or_introl (ex_3 C B T (\lambda (e: C).(\lambda (b: B).(\lambda (v: 
+T).(getl O (CHead c0 (Flat f) t) (CHead e (Bind b) v)))))) (\forall (d: 
+C).((getl O (CHead c0 (Flat f) t) d) \to (\forall (P: Prop).P))) (ex_3_intro 
+C B T (\lambda (e: C).(\lambda (b: B).(\lambda (v: T).(getl O (CHead c0 (Flat 
+f) t) (CHead e (Bind b) v))))) x0 x1 x2 (getl_flat c0 (CHead x0 (Bind x1) x2) 
+O H2 f t))))))) H1)) (\lambda (H1: ((\forall (d: C).((getl O c0 d) \to 
+(\forall (P: Prop).P))))).(or_intror (ex_3 C B T (\lambda (e: C).(\lambda (b: 
+B).(\lambda (v: T).(getl O (CHead c0 (Flat f) t) (CHead e (Bind b) v)))))) 
+(\forall (d: C).((getl O (CHead c0 (Flat f) t) d) \to (\forall (P: Prop).P))) 
+(\lambda (d: C).(\lambda (H2: (getl O (CHead c0 (Flat f) t) d)).(\lambda (P: 
+Prop).(H1 d (getl_intro O c0 d c0 (drop_refl c0) (clear_gen_flat f c0 d t 
+(getl_gen_O (CHead c0 (Flat f) t) d H2))) P)))))) H0)))]) | (S n) \Rightarrow 
+(let H_x \def (H (r k n)) in (let H0 \def H_x in (or_ind (ex_3 C B T (\lambda 
+(e: C).(\lambda (b: B).(\lambda (v: T).(getl (r k n) c0 (CHead e (Bind b) 
+v)))))) (\forall (d: C).((getl (r k n) c0 d) \to (\forall (P: Prop).P))) (or 
+(ex_3 C B T (\lambda (e: C).(\lambda (b: B).(\lambda (v: T).(getl (S n) 
+(CHead c0 k t) (CHead e (Bind b) v)))))) (\forall (d: C).((getl (S n) (CHead 
+c0 k t) d) \to (\forall (P: Prop).P)))) (\lambda (H1: (ex_3 C B T (\lambda 
+(e: C).(\lambda (b: B).(\lambda (v: T).(getl (r k n) c0 (CHead e (Bind b) 
+v))))))).(ex_3_ind C B T (\lambda (e: C).(\lambda (b: B).(\lambda (v: 
+T).(getl (r k n) c0 (CHead e (Bind b) v))))) (or (ex_3 C B T (\lambda (e: 
+C).(\lambda (b: B).(\lambda (v: T).(getl (S n) (CHead c0 k t) (CHead e (Bind 
+b) v)))))) (\forall (d: C).((getl (S n) (CHead c0 k t) d) \to (\forall (P: 
+Prop).P)))) (\lambda (x0: C).(\lambda (x1: B).(\lambda (x2: T).(\lambda (H2: 
+(getl (r k n) c0 (CHead x0 (Bind x1) x2))).(or_introl (ex_3 C B T (\lambda 
+(e: C).(\lambda (b: B).(\lambda (v: T).(getl (S n) (CHead c0 k t) (CHead e 
+(Bind b) v)))))) (\forall (d: C).((getl (S n) (CHead c0 k t) d) \to (\forall 
+(P: Prop).P))) (ex_3_intro C B T (\lambda (e: C).(\lambda (b: B).(\lambda (v: 
+T).(getl (S n) (CHead c0 k t) (CHead e (Bind b) v))))) x0 x1 x2 (getl_head k 
+n c0 (CHead x0 (Bind x1) x2) H2 t))))))) H1)) (\lambda (H1: ((\forall (d: 
+C).((getl (r k n) c0 d) \to (\forall (P: Prop).P))))).(or_intror (ex_3 C B T 
+(\lambda (e: C).(\lambda (b: B).(\lambda (v: T).(getl (S n) (CHead c0 k t) 
+(CHead e (Bind b) v)))))) (\forall (d: C).((getl (S n) (CHead c0 k t) d) \to 
+(\forall (P: Prop).P))) (\lambda (d: C).(\lambda (H2: (getl (S n) (CHead c0 k 
+t) d)).(\lambda (P: Prop).(H1 d (getl_gen_S k c0 d t n H2) P)))))) 
+H0)))])))))) c).
+
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/defs.ma
new file mode 100644 (file)
index 0000000..4084520
--- /dev/null
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/getl/defs".
+
+include "drop/defs.ma".
+
+include "clear/defs.ma".
+
+inductive getl (h:nat) (c1:C) (c2:C): Prop \def
+| getl_intro: \forall (e: C).((drop h O c1 e) \to ((clear e c2) \to (getl h 
+c1 c2))).
+
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/drop.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/drop.ma
new file mode 100644 (file)
index 0000000..593ed87
--- /dev/null
@@ -0,0 +1,66 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/getl/drop".
+
+include "getl/fwd.ma".
+
+include "clear/drop.ma".
+
+include "r/props.ma".
+
+theorem getl_drop:
+ \forall (b: B).(\forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (h: 
+nat).((getl h c (CHead e (Bind b) u)) \to (drop (S h) O c e))))))
+\def
+ \lambda (b: B).(\lambda (c: C).(C_ind (\lambda (c0: C).(\forall (e: 
+C).(\forall (u: T).(\forall (h: nat).((getl h c0 (CHead e (Bind b) u)) \to 
+(drop (S h) O c0 e)))))) (\lambda (n: nat).(\lambda (e: C).(\lambda (u: 
+T).(\lambda (h: nat).(\lambda (H: (getl h (CSort n) (CHead e (Bind b) 
+u))).(getl_gen_sort n h (CHead e (Bind b) u) H (drop (S h) O (CSort n) 
+e))))))) (\lambda (c0: C).(\lambda (H: ((\forall (e: C).(\forall (u: 
+T).(\forall (h: nat).((getl h c0 (CHead e (Bind b) u)) \to (drop (S h) O c0 
+e))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (e: C).(\lambda (u: 
+T).(\lambda (h: nat).(nat_ind (\lambda (n: nat).((getl n (CHead c0 k t) 
+(CHead e (Bind b) u)) \to (drop (S n) O (CHead c0 k t) e))) (\lambda (H0: 
+(getl O (CHead c0 k t) (CHead e (Bind b) u))).(K_ind (\lambda (k0: K).((clear 
+(CHead c0 k0 t) (CHead e (Bind b) u)) \to (drop (S O) O (CHead c0 k0 t) e))) 
+(\lambda (b0: B).(\lambda (H1: (clear (CHead c0 (Bind b0) t) (CHead e (Bind 
+b) u))).(let H2 \def (f_equal C C (\lambda (e0: C).(match e0 in C return 
+(\lambda (_: C).C) with [(CSort _) \Rightarrow e | (CHead c _ _) \Rightarrow 
+c])) (CHead e (Bind b) u) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead 
+e (Bind b) u) t H1)) in ((let H3 \def (f_equal C B (\lambda (e0: C).(match e0 
+in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k _) 
+\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b) 
+\Rightarrow b | (Flat _) \Rightarrow b])])) (CHead e (Bind b) u) (CHead c0 
+(Bind b0) t) (clear_gen_bind b0 c0 (CHead e (Bind b) u) t H1)) in ((let H4 
+\def (f_equal C T (\lambda (e0: C).(match e0 in C return (\lambda (_: C).T) 
+with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead e (Bind 
+b) u) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e (Bind b) u) t 
+H1)) in (\lambda (H5: (eq B b b0)).(\lambda (H6: (eq C e c0)).(eq_ind_r C c0 
+(\lambda (c1: C).(drop (S O) O (CHead c0 (Bind b0) t) c1)) (eq_ind B b 
+(\lambda (b1: B).(drop (S O) O (CHead c0 (Bind b1) t) c0)) (drop_drop (Bind 
+b) O c0 c0 (drop_refl c0) t) b0 H5) e H6)))) H3)) H2)))) (\lambda (f: 
+F).(\lambda (H1: (clear (CHead c0 (Flat f) t) (CHead e (Bind b) 
+u))).(drop_clear_O b (CHead c0 (Flat f) t) e u (clear_flat c0 (CHead e (Bind 
+b) u) (clear_gen_flat f c0 (CHead e (Bind b) u) t H1) f t) e O (drop_refl 
+e)))) k (getl_gen_O (CHead c0 k t) (CHead e (Bind b) u) H0))) (\lambda (n: 
+nat).(\lambda (_: (((getl n (CHead c0 k t) (CHead e (Bind b) u)) \to (drop (S 
+n) O (CHead c0 k t) e)))).(\lambda (H1: (getl (S n) (CHead c0 k t) (CHead e 
+(Bind b) u))).(drop_drop k (S n) c0 e (eq_ind_r nat (S (r k n)) (\lambda (n0: 
+nat).(drop n0 O c0 e)) (H e u (r k n) (getl_gen_S k c0 (CHead e (Bind b) u) t 
+n H1)) (r k (S n)) (r_S k n)) t)))) h)))))))) c)).
+
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/flt.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/flt.ma
new file mode 100644 (file)
index 0000000..589f2dd
--- /dev/null
@@ -0,0 +1,66 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/getl/flt".
+
+include "getl/fwd.ma".
+
+include "clear/props.ma".
+
+include "flt/props.ma".
+
+theorem getl_flt:
+ \forall (b: B).(\forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (i: 
+nat).((getl i c (CHead e (Bind b) u)) \to (flt e u c (TLRef i)))))))
+\def
+ \lambda (b: B).(\lambda (c: C).(C_ind (\lambda (c0: C).(\forall (e: 
+C).(\forall (u: T).(\forall (i: nat).((getl i c0 (CHead e (Bind b) u)) \to 
+(flt e u c0 (TLRef i))))))) (\lambda (n: nat).(\lambda (e: C).(\lambda (u: 
+T).(\lambda (i: nat).(\lambda (H: (getl i (CSort n) (CHead e (Bind b) 
+u))).(getl_gen_sort n i (CHead e (Bind b) u) H (flt e u (CSort n) (TLRef 
+i)))))))) (\lambda (c0: C).(\lambda (H: ((\forall (e: C).(\forall (u: 
+T).(\forall (i: nat).((getl i c0 (CHead e (Bind b) u)) \to (flt e u c0 (TLRef 
+i)))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (e: C).(\lambda (u: 
+T).(\lambda (i: nat).(match i in nat return (\lambda (n: nat).((getl n (CHead 
+c0 k t) (CHead e (Bind b) u)) \to (flt e u (CHead c0 k t) (TLRef n)))) with 
+[O \Rightarrow (\lambda (H0: (getl O (CHead c0 k t) (CHead e (Bind b) 
+u))).((match k in K return (\lambda (k0: K).((clear (CHead c0 k0 t) (CHead e 
+(Bind b) u)) \to (flt e u (CHead c0 k0 t) (TLRef O)))) with [(Bind b0) 
+\Rightarrow (\lambda (H1: (clear (CHead c0 (Bind b0) t) (CHead e (Bind b) 
+u))).(let H2 \def (f_equal C C (\lambda (e0: C).(match e0 in C return 
+(\lambda (_: C).C) with [(CSort _) \Rightarrow e | (CHead c _ _) \Rightarrow 
+c])) (CHead e (Bind b) u) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead 
+e (Bind b) u) t H1)) in ((let H3 \def (f_equal C B (\lambda (e0: C).(match e0 
+in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k _) 
+\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b) 
+\Rightarrow b | (Flat _) \Rightarrow b])])) (CHead e (Bind b) u) (CHead c0 
+(Bind b0) t) (clear_gen_bind b0 c0 (CHead e (Bind b) u) t H1)) in ((let H4 
+\def (f_equal C T (\lambda (e0: C).(match e0 in C return (\lambda (_: C).T) 
+with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead e (Bind 
+b) u) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e (Bind b) u) t 
+H1)) in (\lambda (H5: (eq B b b0)).(\lambda (H6: (eq C e c0)).(eq_ind_r T t 
+(\lambda (t0: T).(flt e t0 (CHead c0 (Bind b0) t) (TLRef O))) (eq_ind_r C c0 
+(\lambda (c1: C).(flt c1 t (CHead c0 (Bind b0) t) (TLRef O))) (eq_ind B b 
+(\lambda (b1: B).(flt c0 t (CHead c0 (Bind b1) t) (TLRef O))) (flt_arith0 
+(Bind b) c0 t O) b0 H5) e H6) u H4)))) H3)) H2))) | (Flat f) \Rightarrow 
+(\lambda (H1: (clear (CHead c0 (Flat f) t) (CHead e (Bind b) u))).(flt_arith1 
+(Bind b) e c0 u (clear_cle c0 (CHead e (Bind b) u) (clear_gen_flat f c0 
+(CHead e (Bind b) u) t H1)) (Flat f) t O))]) (getl_gen_O (CHead c0 k t) 
+(CHead e (Bind b) u) H0))) | (S n) \Rightarrow (\lambda (H0: (getl (S n) 
+(CHead c0 k t) (CHead e (Bind b) u))).(let H_y \def (H e u (r k n) 
+(getl_gen_S k c0 (CHead e (Bind b) u) t n H0)) in (flt_arith2 e c0 u (r k n) 
+H_y k t (S n))))])))))))) c)).
+
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/fwd.ma
new file mode 100644 (file)
index 0000000..afa14d8
--- /dev/null
@@ -0,0 +1,107 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/getl/fwd".
+
+include "getl/defs.ma".
+
+include "drop/fwd.ma".
+
+include "clear/fwd.ma".
+
+theorem getl_gen_all:
+ \forall (c1: C).(\forall (c2: C).(\forall (i: nat).((getl i c1 c2) \to (ex2 
+C (\lambda (e: C).(drop i O c1 e)) (\lambda (e: C).(clear e c2))))))
+\def
+ \lambda (c1: C).(\lambda (c2: C).(\lambda (i: nat).(\lambda (H: (getl i c1 
+c2)).(let H0 \def (match H in getl return (\lambda (_: (getl ? ? ?)).(ex2 C 
+(\lambda (e: C).(drop i O c1 e)) (\lambda (e: C).(clear e c2)))) with 
+[(getl_intro e H0 H1) \Rightarrow (ex_intro2 C (\lambda (e0: C).(drop i O c1 
+e0)) (\lambda (e0: C).(clear e0 c2)) e H0 H1)]) in H0)))).
+
+theorem getl_gen_sort:
+ \forall (n: nat).(\forall (h: nat).(\forall (x: C).((getl h (CSort n) x) \to 
+(\forall (P: Prop).P))))
+\def
+ \lambda (n: nat).(\lambda (h: nat).(\lambda (x: C).(\lambda (H: (getl h 
+(CSort n) x)).(\lambda (P: Prop).(let H0 \def (getl_gen_all (CSort n) x h H) 
+in (ex2_ind C (\lambda (e: C).(drop h O (CSort n) e)) (\lambda (e: C).(clear 
+e x)) P (\lambda (x0: C).(\lambda (H1: (drop h O (CSort n) x0)).(\lambda (H2: 
+(clear x0 x)).(and3_ind (eq C x0 (CSort n)) (eq nat h O) (eq nat O O) P 
+(\lambda (H3: (eq C x0 (CSort n))).(\lambda (_: (eq nat h O)).(\lambda (_: 
+(eq nat O O)).(let H6 \def (eq_ind C x0 (\lambda (c: C).(clear c x)) H2 
+(CSort n) H3) in (clear_gen_sort x n H6 P))))) (drop_gen_sort n h O x0 
+H1))))) H0)))))).
+
+theorem getl_gen_O:
+ \forall (e: C).(\forall (x: C).((getl O e x) \to (clear e x)))
+\def
+ \lambda (e: C).(\lambda (x: C).(\lambda (H: (getl O e x)).(let H0 \def 
+(getl_gen_all e x O H) in (ex2_ind C (\lambda (e0: C).(drop O O e e0)) 
+(\lambda (e0: C).(clear e0 x)) (clear e x) (\lambda (x0: C).(\lambda (H1: 
+(drop O O e x0)).(\lambda (H2: (clear x0 x)).(let H3 \def (eq_ind_r C x0 
+(\lambda (c: C).(clear c x)) H2 e (drop_gen_refl e x0 H1)) in H3)))) H0)))).
+
+theorem getl_gen_S:
+ \forall (k: K).(\forall (c: C).(\forall (x: C).(\forall (u: T).(\forall (h: 
+nat).((getl (S h) (CHead c k u) x) \to (getl (r k h) c x))))))
+\def
+ \lambda (k: K).(\lambda (c: C).(\lambda (x: C).(\lambda (u: T).(\lambda (h: 
+nat).(\lambda (H: (getl (S h) (CHead c k u) x)).(let H0 \def (getl_gen_all 
+(CHead c k u) x (S h) H) in (ex2_ind C (\lambda (e: C).(drop (S h) O (CHead c 
+k u) e)) (\lambda (e: C).(clear e x)) (getl (r k h) c x) (\lambda (x0: 
+C).(\lambda (H1: (drop (S h) O (CHead c k u) x0)).(\lambda (H2: (clear x0 
+x)).(getl_intro (r k h) c x x0 (drop_gen_drop k c x0 u h H1) H2)))) H0))))))).
+
+theorem getl_gen_flat:
+ \forall (f: F).(\forall (e: C).(\forall (d: C).(\forall (v: T).(\forall (i: 
+nat).((getl i (CHead e (Flat f) v) d) \to (getl i e d))))))
+\def
+ \lambda (f: F).(\lambda (e: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: 
+nat).(nat_ind (\lambda (n: nat).((getl n (CHead e (Flat f) v) d) \to (getl n 
+e d))) (\lambda (H: (getl O (CHead e (Flat f) v) d)).(getl_intro O e d e 
+(drop_refl e) (clear_gen_flat f e d v (getl_gen_O (CHead e (Flat f) v) d 
+H)))) (\lambda (n: nat).(\lambda (_: (((getl n (CHead e (Flat f) v) d) \to 
+(getl n e d)))).(\lambda (H0: (getl (S n) (CHead e (Flat f) v) 
+d)).(getl_gen_S (Flat f) e d v n H0)))) i))))).
+
+theorem getl_gen_bind:
+ \forall (b: B).(\forall (e: C).(\forall (d: C).(\forall (v: T).(\forall (i: 
+nat).((getl i (CHead e (Bind b) v) d) \to (or (land (eq nat i O) (eq C d 
+(CHead e (Bind b) v))) (ex2 nat (\lambda (j: nat).(eq nat i (S j))) (\lambda 
+(j: nat).(getl j e d)))))))))
+\def
+ \lambda (b: B).(\lambda (e: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: 
+nat).(nat_ind (\lambda (n: nat).((getl n (CHead e (Bind b) v) d) \to (or 
+(land (eq nat n O) (eq C d (CHead e (Bind b) v))) (ex2 nat (\lambda (j: 
+nat).(eq nat n (S j))) (\lambda (j: nat).(getl j e d)))))) (\lambda (H: (getl 
+O (CHead e (Bind b) v) d)).(eq_ind_r C (CHead e (Bind b) v) (\lambda (c: 
+C).(or (land (eq nat O O) (eq C c (CHead e (Bind b) v))) (ex2 nat (\lambda 
+(j: nat).(eq nat O (S j))) (\lambda (j: nat).(getl j e c))))) (or_introl 
+(land (eq nat O O) (eq C (CHead e (Bind b) v) (CHead e (Bind b) v))) (ex2 nat 
+(\lambda (j: nat).(eq nat O (S j))) (\lambda (j: nat).(getl j e (CHead e 
+(Bind b) v)))) (conj (eq nat O O) (eq C (CHead e (Bind b) v) (CHead e (Bind 
+b) v)) (refl_equal nat O) (refl_equal C (CHead e (Bind b) v)))) d 
+(clear_gen_bind b e d v (getl_gen_O (CHead e (Bind b) v) d H)))) (\lambda (n: 
+nat).(\lambda (_: (((getl n (CHead e (Bind b) v) d) \to (or (land (eq nat n 
+O) (eq C d (CHead e (Bind b) v))) (ex2 nat (\lambda (j: nat).(eq nat n (S 
+j))) (\lambda (j: nat).(getl j e d))))))).(\lambda (H0: (getl (S n) (CHead e 
+(Bind b) v) d)).(or_intror (land (eq nat (S n) O) (eq C d (CHead e (Bind b) 
+v))) (ex2 nat (\lambda (j: nat).(eq nat (S n) (S j))) (\lambda (j: nat).(getl 
+j e d))) (ex_intro2 nat (\lambda (j: nat).(eq nat (S n) (S j))) (\lambda (j: 
+nat).(getl j e d)) n (refl_equal nat (S n)) (getl_gen_S (Bind b) e d v n 
+H0)))))) i))))).
+
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/props.ma
new file mode 100644 (file)
index 0000000..eb20484
--- /dev/null
@@ -0,0 +1,74 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/getl/props".
+
+include "getl/fwd.ma".
+
+include "drop/props.ma".
+
+include "clear/props.ma".
+
+theorem getl_refl:
+ \forall (b: B).(\forall (c: C).(\forall (u: T).(getl O (CHead c (Bind b) u) 
+(CHead c (Bind b) u))))
+\def
+ \lambda (b: B).(\lambda (c: C).(\lambda (u: T).(getl_intro O (CHead c (Bind 
+b) u) (CHead c (Bind b) u) (CHead c (Bind b) u) (drop_refl (CHead c (Bind b) 
+u)) (clear_bind b c u)))).
+
+theorem getl_head:
+ \forall (k: K).(\forall (h: nat).(\forall (c: C).(\forall (e: C).((getl (r k 
+h) c e) \to (\forall (u: T).(getl (S h) (CHead c k u) e))))))
+\def
+ \lambda (k: K).(\lambda (h: nat).(\lambda (c: C).(\lambda (e: C).(\lambda 
+(H: (getl (r k h) c e)).(\lambda (u: T).(let H0 \def (getl_gen_all c e (r k 
+h) H) in (ex2_ind C (\lambda (e0: C).(drop (r k h) O c e0)) (\lambda (e0: 
+C).(clear e0 e)) (getl (S h) (CHead c k u) e) (\lambda (x: C).(\lambda (H1: 
+(drop (r k h) O c x)).(\lambda (H2: (clear x e)).(getl_intro (S h) (CHead c k 
+u) e x (drop_drop k h c x H1 u) H2)))) H0))))))).
+
+theorem getl_flat:
+ \forall (c: C).(\forall (e: C).(\forall (h: nat).((getl h c e) \to (\forall 
+(f: F).(\forall (u: T).(getl h (CHead c (Flat f) u) e))))))
+\def
+ \lambda (c: C).(\lambda (e: C).(\lambda (h: nat).(\lambda (H: (getl h c 
+e)).(\lambda (f: F).(\lambda (u: T).(let H0 \def (getl_gen_all c e h H) in 
+(ex2_ind C (\lambda (e0: C).(drop h O c e0)) (\lambda (e0: C).(clear e0 e)) 
+(getl h (CHead c (Flat f) u) e) (\lambda (x: C).(\lambda (H1: (drop h O c 
+x)).(\lambda (H2: (clear x e)).((match h in nat return (\lambda (n: 
+nat).((drop n O c x) \to (getl n (CHead c (Flat f) u) e))) with [O 
+\Rightarrow (\lambda (H3: (drop O O c x)).(let H4 \def (eq_ind_r C x (\lambda 
+(c: C).(clear c e)) H2 c (drop_gen_refl c x H3)) in (getl_intro O (CHead c 
+(Flat f) u) e (CHead c (Flat f) u) (drop_refl (CHead c (Flat f) u)) 
+(clear_flat c e H4 f u)))) | (S n) \Rightarrow (\lambda (H3: (drop (S n) O c 
+x)).(getl_intro (S n) (CHead c (Flat f) u) e x (drop_drop (Flat f) n c x H3 
+u) H2))]) H1)))) H0))))))).
+
+theorem getl_ctail:
+ \forall (b: B).(\forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i: 
+nat).((getl i c (CHead d (Bind b) u)) \to (\forall (k: K).(\forall (v: 
+T).(getl i (CTail k v c) (CHead (CTail k v d) (Bind b) u)))))))))
+\def
+ \lambda (b: B).(\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: 
+nat).(\lambda (H: (getl i c (CHead d (Bind b) u))).(\lambda (k: K).(\lambda 
+(v: T).(let H0 \def (getl_gen_all c (CHead d (Bind b) u) i H) in (ex2_ind C 
+(\lambda (e: C).(drop i O c e)) (\lambda (e: C).(clear e (CHead d (Bind b) 
+u))) (getl i (CTail k v c) (CHead (CTail k v d) (Bind b) u)) (\lambda (x: 
+C).(\lambda (H1: (drop i O c x)).(\lambda (H2: (clear x (CHead d (Bind b) 
+u))).(getl_intro i (CTail k v c) (CHead (CTail k v d) (Bind b) u) (CTail k v 
+x) (drop_ctail c x O i H1 k v) (clear_ctail b x d u H2 k v))))) H0))))))))).
+
index c0b188265a421764443a20860b5c4f7847f47fe9..7f15aaf0882d01aa6c15858442c5d43da481555e 100644 (file)
@@ -46,6 +46,8 @@ include "r/props.ma".
 
 include "clen/defs.ma".
 
+include "clen/getl.ma".
+
 include "flt/defs.ma".
 
 include "flt/props.ma".
@@ -78,6 +80,30 @@ include "drop1/defs.ma".
 
 include "drop1/props.ma".
 
+include "clear/defs.ma".
+
+include "clear/fwd.ma".
+
+include "clear/props.ma".
+
+include "clear/drop.ma".
+
+include "getl/defs.ma".
+
+include "getl/fwd.ma".
+
+include "getl/props.ma".
+
+include "getl/clear.ma".
+
+include "getl/drop.ma".
+
+include "getl/dec.ma".
+
+include "getl/flt.ma".
+
+include "cimp/defs.ma".
+
 include "G/defs.ma".
 
 include "next_plus/defs.ma".