components/library: dotdothack removed

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / ex2 / props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/props.ma
index 4372ace2dfa69c09e80bdb5fb81af25c4b041ff0..b596f85a2f896c987d390bcd077089f2e3ee2b70 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/props.ma
@@ -141,29 +141,13 @@ Appl) (TSort O) (TSort O)) a)).(\lambda (P: Prop).(let H0 \def
 (a1: A).(arity g (CSort O) (TSort O) a1)) (\lambda (a1: A).(arity g (CSort O) 
 (TSort O) (AHead a1 a))) P (\lambda (x: A).(\lambda (_: (arity g (CSort O) 
 (TSort O) x)).(\lambda (H2: (arity g (CSort O) (TSort O) (AHead x a))).(let 
-H3 \def (match (arity_gen_sort g (CSort O) O (AHead x a) H2) in leq return 
-(\lambda (a0: A).(\lambda (a1: A).(\lambda (_: (leq ? a0 a1)).((eq A a0 
-(AHead x a)) \to ((eq A a1 (ASort O O)) \to P))))) with [(leq_sort h1 h2 n1 
-n2 k H3) \Rightarrow (\lambda (H4: (eq A (ASort h1 n1) (AHead x a))).(\lambda 
-(H5: (eq A (ASort h2 n2) (ASort O O))).((let H6 \def (eq_ind A (ASort h1 n1) 
-(\lambda (e: A).(match e in A return (\lambda (_: A).Prop) with [(ASort _ _) 
-\Rightarrow True | (AHead _ _) \Rightarrow False])) I (AHead x a) H4) in 
-(False_ind ((eq A (ASort h2 n2) (ASort O O)) \to ((eq A (aplus g (ASort h1 
-n1) k) (aplus g (ASort h2 n2) k)) \to P)) H6)) H5 H3))) | (leq_head a1 a2 H3 
-a3 a4 H4) \Rightarrow (\lambda (H5: (eq A (AHead a1 a3) (AHead x 
-a))).(\lambda (H6: (eq A (AHead a2 a4) (ASort O O))).((let H7 \def (f_equal A 
-A (\lambda (e: A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) 
-\Rightarrow a3 | (AHead _ a0) \Rightarrow a0])) (AHead a1 a3) (AHead x a) H5) 
-in ((let H8 \def (f_equal A A (\lambda (e: A).(match e in A return (\lambda 
-(_: A).A) with [(ASort _ _) \Rightarrow a1 | (AHead a0 _) \Rightarrow a0])) 
-(AHead a1 a3) (AHead x a) H5) in (eq_ind A x (\lambda (a0: A).((eq A a3 a) 
-\to ((eq A (AHead a2 a4) (ASort O O)) \to ((leq g a0 a2) \to ((leq g a3 a4) 
-\to P))))) (\lambda (H9: (eq A a3 a)).(eq_ind A a (\lambda (a0: A).((eq A 
-(AHead a2 a4) (ASort O O)) \to ((leq g x a2) \to ((leq g a0 a4) \to P)))) 
-(\lambda (H10: (eq A (AHead a2 a4) (ASort O O))).(let H11 \def (eq_ind A 
-(AHead a2 a4) (\lambda (e: A).(match e in A return (\lambda (_: A).Prop) with 
-[(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow True])) I (ASort O 
-O) H10) in (False_ind ((leq g x a2) \to ((leq g a a4) \to P)) H11))) a3 
-(sym_eq A a3 a H9))) a1 (sym_eq A a1 x H8))) H7)) H6 H3 H4)))]) in (H3 
-(refl_equal A (AHead x a)) (refl_equal A (ASort O O))))))) H0))))).
+H_x \def (leq_gen_head1 g x a (ASort O O) (arity_gen_sort g (CSort O) O 
+(AHead x a) H2)) in (let H3 \def H_x in (ex3_2_ind A A (\lambda (a3: 
+A).(\lambda (_: A).(leq g x a3))) (\lambda (_: A).(\lambda (a4: A).(leq g a 
+a4))) (\lambda (a3: A).(\lambda (a4: A).(eq A (ASort O O) (AHead a3 a4)))) P 
+(\lambda (x0: A).(\lambda (x1: A).(\lambda (_: (leq g x x0)).(\lambda (_: 
+(leq g a x1)).(\lambda (H6: (eq A (ASort O O) (AHead x0 x1))).(let H7 \def 
+(eq_ind A (ASort O O) (\lambda (ee: A).(match ee in A return (\lambda (_: 
+A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _) \Rightarrow 
+False])) I (AHead x0 x1) H6) in (False_ind P H7))))))) H3)))))) H0))))).