X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Faprem%2Fprops.ma;h=895bc51769029100b2a8e254d52ae35eb06e14eb;hb=f5dfc6c24a393a4717a7b40689df768d271d9ac0;hp=0a0a9525e6b50356214c00e6a4d8caa984e32cad;hpb=e92710b1d9774a6491122668c8463b8658114610;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/props.ma
index 0a0a9525e..895bc5176 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/aprem/defs.ma".
+include "LambdaDelta-1/aprem/fwd.ma".
 
 include "LambdaDelta-1/leq/defs.ma".
 
@@ -29,111 +29,32 @@ a2)).(leq_ind g (\lambda (a: A).(\lambda (a0: A).(\forall (i: nat).(\forall
 (b1: A).(aprem i a b1)))))))) (\lambda (h1: nat).(\lambda (h2: nat).(\lambda 
 (n1: nat).(\lambda (n2: nat).(\lambda (k: nat).(\lambda (_: (eq A (aplus g 
 (ASort h1 n1) k) (aplus g (ASort h2 n2) k))).(\lambda (i: nat).(\lambda (b2: 
-A).(\lambda (H1: (aprem i (ASort h2 n2) b2)).(let H2 \def (match H1 in aprem 
-return (\lambda (n: nat).(\lambda (a: A).(\lambda (a0: A).(\lambda (_: (aprem 
-n a a0)).((eq nat n i) \to ((eq A a (ASort h2 n2)) \to ((eq A a0 b2) \to (ex2 
-A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem i (ASort h1 n1) 
-b1)))))))))) with [(aprem_zero a0 a3) \Rightarrow (\lambda (H2: (eq nat O 
-i)).(\lambda (H3: (eq A (AHead a0 a3) (ASort h2 n2))).(\lambda (H4: (eq A a0 
-b2)).(eq_ind nat O (\lambda (n: nat).((eq A (AHead a0 a3) (ASort h2 n2)) \to 
-((eq A a0 b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: 
-A).(aprem n (ASort h1 n1) b1)))))) (\lambda (H5: (eq A (AHead a0 a3) (ASort 
-h2 n2))).(let H6 \def (eq_ind A (AHead a0 a3) (\lambda (e: A).(match e in A 
-return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ 
-_) \Rightarrow True])) I (ASort h2 n2) H5) in (False_ind ((eq A a0 b2) \to 
-(ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem O (ASort h1 
-n1) b1)))) H6))) i H2 H3 H4)))) | (aprem_succ a0 a i0 H2 a3) \Rightarrow 
-(\lambda (H3: (eq nat (S i0) i)).(\lambda (H4: (eq A (AHead a3 a0) (ASort h2 
-n2))).(\lambda (H5: (eq A a b2)).(eq_ind nat (S i0) (\lambda (n: nat).((eq A 
-(AHead a3 a0) (ASort h2 n2)) \to ((eq A a b2) \to ((aprem i0 a0 a) \to (ex2 A 
-(\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem n (ASort h1 n1) 
-b1))))))) (\lambda (H6: (eq A (AHead a3 a0) (ASort h2 n2))).(let H7 \def 
-(eq_ind A (AHead a3 a0) (\lambda (e: A).(match e in A return (\lambda (_: 
-A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow 
-True])) I (ASort h2 n2) H6) in (False_ind ((eq A a b2) \to ((aprem i0 a0 a) 
-\to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S i0) 
-(ASort h1 n1) b1))))) H7))) i H3 H4 H5 H2))))]) in (H2 (refl_equal nat i) 
-(refl_equal A (ASort h2 n2)) (refl_equal A b2)))))))))))) (\lambda (a0: 
-A).(\lambda (a3: A).(\lambda (H0: (leq g a0 a3)).(\lambda (_: ((\forall (i: 
-nat).(\forall (b2: A).((aprem i a3 b2) \to (ex2 A (\lambda (b1: A).(leq g b1 
-b2)) (\lambda (b1: A).(aprem i a0 b1)))))))).(\lambda (a4: A).(\lambda (a5: 
-A).(\lambda (_: (leq g a4 a5)).(\lambda (H3: ((\forall (i: nat).(\forall (b2: 
-A).((aprem i a5 b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: 
-A).(aprem i a4 b1)))))))).(\lambda (i: nat).(\lambda (b2: A).(\lambda (H4: 
-(aprem i (AHead a3 a5) b2)).(nat_ind (\lambda (n: nat).((aprem n (AHead a3 
-a5) b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem n 
-(AHead a0 a4) b1))))) (\lambda (H5: (aprem O (AHead a3 a5) b2)).(let H6 \def 
-(match H5 in aprem return (\lambda (n: nat).(\lambda (a: A).(\lambda (a6: 
-A).(\lambda (_: (aprem n a a6)).((eq nat n O) \to ((eq A a (AHead a3 a5)) \to 
-((eq A a6 b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: 
-A).(aprem O (AHead a0 a4) b1)))))))))) with [(aprem_zero a6 a7) \Rightarrow 
-(\lambda (_: (eq nat O O)).(\lambda (H7: (eq A (AHead a6 a7) (AHead a3 
-a5))).(\lambda (H8: (eq A a6 b2)).((let H9 \def (f_equal A A (\lambda (e: 
-A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a7 | 
-(AHead _ a) \Rightarrow a])) (AHead a6 a7) (AHead a3 a5) H7) in ((let H10 
-\def (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) 
-with [(ASort _ _) \Rightarrow a6 | (AHead a _) \Rightarrow a])) (AHead a6 a7) 
-(AHead a3 a5) H7) in (eq_ind A a3 (\lambda (a: A).((eq A a7 a5) \to ((eq A a 
-b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem O 
-(AHead a0 a4) b1)))))) (\lambda (H11: (eq A a7 a5)).(eq_ind A a5 (\lambda (_: 
-A).((eq A a3 b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: 
-A).(aprem O (AHead a0 a4) b1))))) (\lambda (H12: (eq A a3 b2)).(eq_ind A b2 
-(\lambda (_: A).(ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: 
-A).(aprem O (AHead a0 a4) b1)))) (eq_ind A a3 (\lambda (a: A).(ex2 A (\lambda 
-(b1: A).(leq g b1 a)) (\lambda (b1: A).(aprem O (AHead a0 a4) b1)))) 
+A).(\lambda (H1: (aprem i (ASort h2 n2) b2)).(let H_x \def (aprem_gen_sort b2 
+i h2 n2 H1) in (let H2 \def H_x in (False_ind (ex2 A (\lambda (b1: A).(leq g 
+b1 b2)) (\lambda (b1: A).(aprem i (ASort h1 n1) b1))) H2)))))))))))) (\lambda 
+(a0: A).(\lambda (a3: A).(\lambda (H0: (leq g a0 a3)).(\lambda (_: ((\forall 
+(i: nat).(\forall (b2: A).((aprem i a3 b2) \to (ex2 A (\lambda (b1: A).(leq g 
+b1 b2)) (\lambda (b1: A).(aprem i a0 b1)))))))).(\lambda (a4: A).(\lambda 
+(a5: A).(\lambda (_: (leq g a4 a5)).(\lambda (H3: ((\forall (i: nat).(\forall 
+(b2: A).((aprem i a5 b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda 
+(b1: A).(aprem i a4 b1)))))))).(\lambda (i: nat).(\lambda (b2: A).(\lambda 
+(H4: (aprem i (AHead a3 a5) b2)).(nat_ind (\lambda (n: nat).((aprem n (AHead 
+a3 a5) b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem 
+n (AHead a0 a4) b1))))) (\lambda (H5: (aprem O (AHead a3 a5) b2)).(let H_y 
+\def (aprem_gen_head_O a3 a5 b2 H5) in (eq_ind_r A a3 (\lambda (a: A).(ex2 A 
+(\lambda (b1: A).(leq g b1 a)) (\lambda (b1: A).(aprem O (AHead a0 a4) b1)))) 
 (ex_intro2 A (\lambda (b1: A).(leq g b1 a3)) (\lambda (b1: A).(aprem O (AHead 
-a0 a4) b1)) a0 H0 (aprem_zero a0 a4)) b2 H12) a3 (sym_eq A a3 b2 H12))) a7 
-(sym_eq A a7 a5 H11))) a6 (sym_eq A a6 a3 H10))) H9)) H8)))) | (aprem_succ a6 
-a i0 H6 a7) \Rightarrow (\lambda (H7: (eq nat (S i0) O)).(\lambda (H8: (eq A 
-(AHead a7 a6) (AHead a3 a5))).(\lambda (H9: (eq A a b2)).((let H10 \def 
-(eq_ind nat (S i0) (\lambda (e: nat).(match e in nat return (\lambda (_: 
-nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H7) in 
-(False_ind ((eq A (AHead a7 a6) (AHead a3 a5)) \to ((eq A a b2) \to ((aprem 
-i0 a6 a) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem O 
-(AHead a0 a4) b1)))))) H10)) H8 H9 H6))))]) in (H6 (refl_equal nat O) 
-(refl_equal A (AHead a3 a5)) (refl_equal A b2)))) (\lambda (i0: nat).(\lambda 
+a0 a4) b1)) a0 H0 (aprem_zero a0 a4)) b2 H_y))) (\lambda (i0: nat).(\lambda 
 (_: (((aprem i0 (AHead a3 a5) b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) 
 (\lambda (b1: A).(aprem i0 (AHead a0 a4) b1)))))).(\lambda (H5: (aprem (S i0) 
-(AHead a3 a5) b2)).(let H6 \def (match H5 in aprem return (\lambda (n: 
-nat).(\lambda (a: A).(\lambda (a6: A).(\lambda (_: (aprem n a a6)).((eq nat n 
-(S i0)) \to ((eq A a (AHead a3 a5)) \to ((eq A a6 b2) \to (ex2 A (\lambda 
-(b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S i0) (AHead a0 a4) 
-b1)))))))))) with [(aprem_zero a6 a7) \Rightarrow (\lambda (H6: (eq nat O (S 
-i0))).(\lambda (H7: (eq A (AHead a6 a7) (AHead a3 a5))).(\lambda (H8: (eq A 
-a6 b2)).((let H9 \def (eq_ind nat O (\lambda (e: nat).(match e in nat return 
-(\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False])) 
-I (S i0) H6) in (False_ind ((eq A (AHead a6 a7) (AHead a3 a5)) \to ((eq A a6 
-b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S i0) 
-(AHead a0 a4) b1))))) H9)) H7 H8)))) | (aprem_succ a6 a i1 H6 a7) \Rightarrow 
-(\lambda (H7: (eq nat (S i1) (S i0))).(\lambda (H8: (eq A (AHead a7 a6) 
-(AHead a3 a5))).(\lambda (H9: (eq A a b2)).((let H10 \def (f_equal nat nat 
-(\lambda (e: nat).(match e in nat return (\lambda (_: nat).nat) with [O 
-\Rightarrow i1 | (S n) \Rightarrow n])) (S i1) (S i0) H7) in (eq_ind nat i0 
-(\lambda (n: nat).((eq A (AHead a7 a6) (AHead a3 a5)) \to ((eq A a b2) \to 
-((aprem n a6 a) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: 
-A).(aprem (S i0) (AHead a0 a4) b1))))))) (\lambda (H11: (eq A (AHead a7 a6) 
-(AHead a3 a5))).(let H12 \def (f_equal A A (\lambda (e: A).(match e in A 
-return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a6 | (AHead _ a8) 
-\Rightarrow a8])) (AHead a7 a6) (AHead a3 a5) H11) in ((let H13 \def (f_equal 
-A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) 
-\Rightarrow a7 | (AHead a8 _) \Rightarrow a8])) (AHead a7 a6) (AHead a3 a5) 
-H11) in (eq_ind A a3 (\lambda (_: A).((eq A a6 a5) \to ((eq A a b2) \to 
-((aprem i0 a6 a) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: 
-A).(aprem (S i0) (AHead a0 a4) b1))))))) (\lambda (H14: (eq A a6 a5)).(eq_ind 
-A a5 (\lambda (a8: A).((eq A a b2) \to ((aprem i0 a8 a) \to (ex2 A (\lambda 
-(b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S i0) (AHead a0 a4) b1)))))) 
-(\lambda (H15: (eq A a b2)).(eq_ind A b2 (\lambda (a8: A).((aprem i0 a5 a8) 
-\to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S i0) 
-(AHead a0 a4) b1))))) (\lambda (H16: (aprem i0 a5 b2)).(let H_x \def (H3 i0 
-b2 H16) in (let H17 \def H_x in (ex2_ind A (\lambda (b1: A).(leq g b1 b2)) 
-(\lambda (b1: A).(aprem i0 a4 b1)) (ex2 A (\lambda (b1: A).(leq g b1 b2)) 
-(\lambda (b1: A).(aprem (S i0) (AHead a0 a4) b1))) (\lambda (x: A).(\lambda 
-(H18: (leq g x b2)).(\lambda (H19: (aprem i0 a4 x)).(ex_intro2 A (\lambda 
-(b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S i0) (AHead a0 a4) b1)) x 
-H18 (aprem_succ a4 x i0 H19 a0))))) H17)))) a (sym_eq A a b2 H15))) a6 
-(sym_eq A a6 a5 H14))) a7 (sym_eq A a7 a3 H13))) H12))) i1 (sym_eq nat i1 i0 
-H10))) H8 H9 H6))))]) in (H6 (refl_equal nat (S i0)) (refl_equal A (AHead a3 
-a5)) (refl_equal A b2)))))) i H4)))))))))))) a1 a2 H)))).
+(AHead a3 a5) b2)).(let H_y \def (aprem_gen_head_S a3 a5 b2 i0 H5) in (let 
+H_x \def (H3 i0 b2 H_y) in (let H6 \def H_x in (ex2_ind A (\lambda (b1: 
+A).(leq g b1 b2)) (\lambda (b1: A).(aprem i0 a4 b1)) (ex2 A (\lambda (b1: 
+A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S i0) (AHead a0 a4) b1))) (\lambda 
+(x: A).(\lambda (H7: (leq g x b2)).(\lambda (H8: (aprem i0 a4 x)).(ex_intro2 
+A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S i0) (AHead a0 
+a4) b1)) x H7 (aprem_succ a4 x i0 H8 a0))))) H6))))))) i H4)))))))))))) a1 a2 
+H)))).
 
 theorem aprem_asucc:
  \forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (i: nat).((aprem i