]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_1/asucc/fwd.ma
update in static_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / asucc / fwd.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "basic_1/asucc/defs.ma".
18
19 include "basic_1/A/fwd.ma".
20
21 lemma asucc_gen_sort:
22  \forall (g: G).(\forall (h: nat).(\forall (n: nat).(\forall (a: A).((eq A 
23 (ASort h n) (asucc g a)) \to (ex_2 nat nat (\lambda (h0: nat).(\lambda (n0: 
24 nat).(eq A a (ASort h0 n0)))))))))
25 \def
26  \lambda (g: G).(\lambda (h: nat).(\lambda (n: nat).(\lambda (a: A).(A_ind 
27 (\lambda (a0: A).((eq A (ASort h n) (asucc g a0)) \to (ex_2 nat nat (\lambda 
28 (h0: nat).(\lambda (n0: nat).(eq A a0 (ASort h0 n0))))))) (\lambda (n0: 
29 nat).(\lambda (n1: nat).(\lambda (H: (eq A (ASort h n) (asucc g (ASort n0 
30 n1)))).(let H0 \def (f_equal A A (\lambda (e: A).e) (ASort h n) (match n0 
31 with [O \Rightarrow (ASort O (next g n1)) | (S h0) \Rightarrow (ASort h0 
32 n1)]) H) in (ex_2_intro nat nat (\lambda (h0: nat).(\lambda (n2: nat).(eq A 
33 (ASort n0 n1) (ASort h0 n2)))) n0 n1 (refl_equal A (ASort n0 n1))))))) 
34 (\lambda (a0: A).(\lambda (_: (((eq A (ASort h n) (asucc g a0)) \to (ex_2 nat 
35 nat (\lambda (h0: nat).(\lambda (n0: nat).(eq A a0 (ASort h0 
36 n0)))))))).(\lambda (a1: A).(\lambda (_: (((eq A (ASort h n) (asucc g a1)) 
37 \to (ex_2 nat nat (\lambda (h0: nat).(\lambda (n0: nat).(eq A a1 (ASort h0 
38 n0)))))))).(\lambda (H1: (eq A (ASort h n) (asucc g (AHead a0 a1)))).(let H2 
39 \def (eq_ind A (ASort h n) (\lambda (ee: A).(match ee with [(ASort _ _) 
40 \Rightarrow True | (AHead _ _) \Rightarrow False])) I (asucc g (AHead a0 a1)) 
41 H1) in (False_ind (ex_2 nat nat (\lambda (h0: nat).(\lambda (n0: nat).(eq A 
42 (AHead a0 a1) (ASort h0 n0))))) H2))))))) a)))).
43
44 lemma asucc_gen_head:
45  \forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (a: A).((eq A 
46 (AHead a1 a2) (asucc g a)) \to (ex2 A (\lambda (a0: A).(eq A a (AHead a1 
47 a0))) (\lambda (a0: A).(eq A a2 (asucc g a0))))))))
48 \def
49  \lambda (g: G).(\lambda (a1: A).(\lambda (a2: A).(\lambda (a: A).(A_ind 
50 (\lambda (a0: A).((eq A (AHead a1 a2) (asucc g a0)) \to (ex2 A (\lambda (a3: 
51 A).(eq A a0 (AHead a1 a3))) (\lambda (a3: A).(eq A a2 (asucc g a3)))))) 
52 (\lambda (n: nat).(\lambda (n0: nat).(\lambda (H: (eq A (AHead a1 a2) (asucc 
53 g (ASort n n0)))).(nat_ind (\lambda (n1: nat).((eq A (AHead a1 a2) (asucc g 
54 (ASort n1 n0))) \to (ex2 A (\lambda (a0: A).(eq A (ASort n1 n0) (AHead a1 
55 a0))) (\lambda (a0: A).(eq A a2 (asucc g a0)))))) (\lambda (H0: (eq A (AHead 
56 a1 a2) (asucc g (ASort O n0)))).(let H1 \def (eq_ind A (AHead a1 a2) (\lambda 
57 (ee: A).(match ee with [(ASort _ _) \Rightarrow False | (AHead _ _) 
58 \Rightarrow True])) I (ASort O (next g n0)) H0) in (False_ind (ex2 A (\lambda 
59 (a0: A).(eq A (ASort O n0) (AHead a1 a0))) (\lambda (a0: A).(eq A a2 (asucc g 
60 a0)))) H1))) (\lambda (n1: nat).(\lambda (_: (((eq A (AHead a1 a2) (asucc g 
61 (ASort n1 n0))) \to (ex2 A (\lambda (a0: A).(eq A (ASort n1 n0) (AHead a1 
62 a0))) (\lambda (a0: A).(eq A a2 (asucc g a0))))))).(\lambda (H0: (eq A (AHead 
63 a1 a2) (asucc g (ASort (S n1) n0)))).(let H1 \def (eq_ind A (AHead a1 a2) 
64 (\lambda (ee: A).(match ee with [(ASort _ _) \Rightarrow False | (AHead _ _) 
65 \Rightarrow True])) I (ASort n1 n0) H0) in (False_ind (ex2 A (\lambda (a0: 
66 A).(eq A (ASort (S n1) n0) (AHead a1 a0))) (\lambda (a0: A).(eq A a2 (asucc g 
67 a0)))) H1))))) n H)))) (\lambda (a0: A).(\lambda (H: (((eq A (AHead a1 a2) 
68 (asucc g a0)) \to (ex2 A (\lambda (a3: A).(eq A a0 (AHead a1 a3))) (\lambda 
69 (a3: A).(eq A a2 (asucc g a3))))))).(\lambda (a3: A).(\lambda (H0: (((eq A 
70 (AHead a1 a2) (asucc g a3)) \to (ex2 A (\lambda (a4: A).(eq A a3 (AHead a1 
71 a4))) (\lambda (a4: A).(eq A a2 (asucc g a4))))))).(\lambda (H1: (eq A (AHead 
72 a1 a2) (asucc g (AHead a0 a3)))).(let H2 \def (f_equal A A (\lambda (e: 
73 A).(match e with [(ASort _ _) \Rightarrow a1 | (AHead a4 _) \Rightarrow a4])) 
74 (AHead a1 a2) (AHead a0 (asucc g a3)) H1) in ((let H3 \def (f_equal A A 
75 (\lambda (e: A).(match e with [(ASort _ _) \Rightarrow a2 | (AHead _ a4) 
76 \Rightarrow a4])) (AHead a1 a2) (AHead a0 (asucc g a3)) H1) in (\lambda (H4: 
77 (eq A a1 a0)).(let H5 \def (eq_ind_r A a0 (\lambda (a4: A).((eq A (AHead a1 
78 a2) (asucc g a4)) \to (ex2 A (\lambda (a5: A).(eq A a4 (AHead a1 a5))) 
79 (\lambda (a5: A).(eq A a2 (asucc g a5)))))) H a1 H4) in (eq_ind A a1 (\lambda 
80 (a4: A).(ex2 A (\lambda (a5: A).(eq A (AHead a4 a3) (AHead a1 a5))) (\lambda 
81 (a5: A).(eq A a2 (asucc g a5))))) (let H6 \def (eq_ind A a2 (\lambda (a4: 
82 A).((eq A (AHead a1 a4) (asucc g a3)) \to (ex2 A (\lambda (a5: A).(eq A a3 
83 (AHead a1 a5))) (\lambda (a5: A).(eq A a4 (asucc g a5)))))) H0 (asucc g a3) 
84 H3) in (let H7 \def (eq_ind A a2 (\lambda (a4: A).((eq A (AHead a1 a4) (asucc 
85 g a1)) \to (ex2 A (\lambda (a5: A).(eq A a1 (AHead a1 a5))) (\lambda (a5: 
86 A).(eq A a4 (asucc g a5)))))) H5 (asucc g a3) H3) in (eq_ind_r A (asucc g a3) 
87 (\lambda (a4: A).(ex2 A (\lambda (a5: A).(eq A (AHead a1 a3) (AHead a1 a5))) 
88 (\lambda (a5: A).(eq A a4 (asucc g a5))))) (ex_intro2 A (\lambda (a4: A).(eq 
89 A (AHead a1 a3) (AHead a1 a4))) (\lambda (a4: A).(eq A (asucc g a3) (asucc g 
90 a4))) a3 (refl_equal A (AHead a1 a3)) (refl_equal A (asucc g a3))) a2 H3))) 
91 a0 H4)))) H2))))))) a)))).
92