(* This file was automatically generated: do not edit *********************)
+include "LambdaDelta-1/ex2/defs.ma".
+include "LambdaDelta-1/nf2/defs.ma".
-include "ex2/defs.ma".
+include "LambdaDelta-1/pr2/fwd.ma".
-include "nf2/defs.ma".
-
-include "pr2/fwd.ma".
-
-include "arity/fwd.ma".
+include "LambdaDelta-1/arity/fwd.ma".
theorem ex2_nf2:
nf2 ex2_c ex2_t
(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))))).