]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_1/wf3/getl.ma
news for matita 0.99.3
[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / wf3 / getl.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/wf3/clear.ma".
18
19 include "basic_1/ty3/dec.ma".
20
21 lemma wf3_getl_conf:
22  \forall (b: B).(\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall 
23 (v: T).((getl i c1 (CHead d1 (Bind b) v)) \to (\forall (g: G).(\forall (c2: 
24 C).((wf3 g c1 c2) \to (\forall (w: T).((ty3 g d1 v w) \to (ex2 C (\lambda 
25 (d2: C).(getl i c2 (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 
26 d2)))))))))))))
27 \def
28  \lambda (b: B).(\lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: 
29 C).(\forall (d1: C).(\forall (v: T).((getl n c1 (CHead d1 (Bind b) v)) \to 
30 (\forall (g: G).(\forall (c2: C).((wf3 g c1 c2) \to (\forall (w: T).((ty3 g 
31 d1 v w) \to (ex2 C (\lambda (d2: C).(getl n c2 (CHead d2 (Bind b) v))) 
32 (\lambda (d2: C).(wf3 g d1 d2))))))))))))) (\lambda (c1: C).(\lambda (d1: 
33 C).(\lambda (v: T).(\lambda (H: (getl O c1 (CHead d1 (Bind b) v))).(\lambda 
34 (g: G).(\lambda (c2: C).(\lambda (H0: (wf3 g c1 c2)).(\lambda (w: T).(\lambda 
35 (H1: (ty3 g d1 v w)).(let H_y \def (wf3_clear_conf c1 (CHead d1 (Bind b) v) 
36 (getl_gen_O c1 (CHead d1 (Bind b) v) H) g c2 H0) in (let H_x \def 
37 (wf3_gen_bind1 g d1 c2 v b H_y) in (let H2 \def H_x in (or_ind (ex3_2 C T 
38 (\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda 
39 (c3: C).(\lambda (_: T).(wf3 g d1 c3))) (\lambda (_: C).(\lambda (w0: T).(ty3 
40 g d1 v w0)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort 
41 O)))) (\lambda (c3: C).(wf3 g d1 c3)) (\lambda (_: C).(\forall (w0: T).((ty3 
42 g d1 v w0) \to False)))) (ex2 C (\lambda (d2: C).(getl O c2 (CHead d2 (Bind 
43 b) v))) (\lambda (d2: C).(wf3 g d1 d2))) (\lambda (H3: (ex3_2 C T (\lambda 
44 (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda (c3: 
45 C).(\lambda (_: T).(wf3 g d1 c3))) (\lambda (_: C).(\lambda (w0: T).(ty3 g d1 
46 v w0))))).(ex3_2_ind C T (\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 
47 (Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g d1 c3))) (\lambda (_: 
48 C).(\lambda (w0: T).(ty3 g d1 v w0))) (ex2 C (\lambda (d2: C).(getl O c2 
49 (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2))) (\lambda (x0: 
50 C).(\lambda (x1: T).(\lambda (H4: (eq C c2 (CHead x0 (Bind b) v))).(\lambda 
51 (H5: (wf3 g d1 x0)).(\lambda (_: (ty3 g d1 v x1)).(eq_ind_r C (CHead x0 (Bind 
52 b) v) (\lambda (c: C).(ex2 C (\lambda (d2: C).(getl O c (CHead d2 (Bind b) 
53 v))) (\lambda (d2: C).(wf3 g d1 d2)))) (ex_intro2 C (\lambda (d2: C).(getl O 
54 (CHead x0 (Bind b) v) (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)) 
55 x0 (getl_refl b x0 v) H5) c2 H4)))))) H3)) (\lambda (H3: (ex3 C (\lambda (c3: 
56 C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g d1 
57 c3)) (\lambda (_: C).(\forall (w0: T).((ty3 g d1 v w0) \to 
58 False))))).(ex3_ind C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort 
59 O)))) (\lambda (c3: C).(wf3 g d1 c3)) (\lambda (_: C).(\forall (w0: T).((ty3 
60 g d1 v w0) \to False))) (ex2 C (\lambda (d2: C).(getl O c2 (CHead d2 (Bind b) 
61 v))) (\lambda (d2: C).(wf3 g d1 d2))) (\lambda (x0: C).(\lambda (H4: (eq C c2 
62 (CHead x0 (Bind Void) (TSort O)))).(\lambda (_: (wf3 g d1 x0)).(\lambda (H6: 
63 ((\forall (w0: T).((ty3 g d1 v w0) \to False)))).(eq_ind_r C (CHead x0 (Bind 
64 Void) (TSort O)) (\lambda (c: C).(ex2 C (\lambda (d2: C).(getl O c (CHead d2 
65 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)))) (let H_x0 \def (H6 w H1) in 
66 (let H7 \def H_x0 in (False_ind (ex2 C (\lambda (d2: C).(getl O (CHead x0 
67 (Bind Void) (TSort O)) (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 
68 d2))) H7))) c2 H4))))) H3)) H2))))))))))))) (\lambda (n: nat).(\lambda (H: 
69 ((\forall (c1: C).(\forall (d1: C).(\forall (v: T).((getl n c1 (CHead d1 
70 (Bind b) v)) \to (\forall (g: G).(\forall (c2: C).((wf3 g c1 c2) \to (\forall 
71 (w: T).((ty3 g d1 v w) \to (ex2 C (\lambda (d2: C).(getl n c2 (CHead d2 (Bind 
72 b) v))) (\lambda (d2: C).(wf3 g d1 d2)))))))))))))).(\lambda (c1: C).(C_ind 
73 (\lambda (c: C).(\forall (d1: C).(\forall (v: T).((getl (S n) c (CHead d1 
74 (Bind b) v)) \to (\forall (g: G).(\forall (c2: C).((wf3 g c c2) \to (\forall 
75 (w: T).((ty3 g d1 v w) \to (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 
76 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)))))))))))) (\lambda (n0: 
77 nat).(\lambda (d1: C).(\lambda (v: T).(\lambda (H0: (getl (S n) (CSort n0) 
78 (CHead d1 (Bind b) v))).(\lambda (g: G).(\lambda (c2: C).(\lambda (_: (wf3 g 
79 (CSort n0) c2)).(\lambda (w: T).(\lambda (_: (ty3 g d1 v w)).(getl_gen_sort 
80 n0 (S n) (CHead d1 (Bind b) v) H0 (ex2 C (\lambda (d2: C).(getl (S n) c2 
81 (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2))))))))))))) (\lambda 
82 (c: C).(\lambda (H0: ((\forall (d1: C).(\forall (v: T).((getl (S n) c (CHead 
83 d1 (Bind b) v)) \to (\forall (g: G).(\forall (c2: C).((wf3 g c c2) \to 
84 (\forall (w: T).((ty3 g d1 v w) \to (ex2 C (\lambda (d2: C).(getl (S n) c2 
85 (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2))))))))))))).(\lambda 
86 (k: K).(\lambda (t: T).(\lambda (d1: C).(\lambda (v: T).(\lambda (H1: (getl 
87 (S n) (CHead c k t) (CHead d1 (Bind b) v))).(\lambda (g: G).(\lambda (c2: 
88 C).(\lambda (H2: (wf3 g (CHead c k t) c2)).(\lambda (w: T).(\lambda (H3: (ty3 
89 g d1 v w)).(K_ind (\lambda (k0: K).((wf3 g (CHead c k0 t) c2) \to ((getl (r 
90 k0 n) c (CHead d1 (Bind b) v)) \to (ex2 C (\lambda (d2: C).(getl (S n) c2 
91 (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)))))) (\lambda (b0: 
92 B).(\lambda (H4: (wf3 g (CHead c (Bind b0) t) c2)).(\lambda (H5: (getl (r 
93 (Bind b0) n) c (CHead d1 (Bind b) v))).(let H_x \def (wf3_gen_bind1 g c c2 t 
94 b0 H4) in (let H6 \def H_x in (or_ind (ex3_2 C T (\lambda (c3: C).(\lambda 
95 (_: T).(eq C c2 (CHead c3 (Bind b0) t)))) (\lambda (c3: C).(\lambda (_: 
96 T).(wf3 g c c3))) (\lambda (_: C).(\lambda (w0: T).(ty3 g c t w0)))) (ex3 C 
97 (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: 
98 C).(wf3 g c c3)) (\lambda (_: C).(\forall (w0: T).((ty3 g c t w0) \to 
99 False)))) (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind b) v))) 
100 (\lambda (d2: C).(wf3 g d1 d2))) (\lambda (H7: (ex3_2 C T (\lambda (c3: 
101 C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b0) t)))) (\lambda (c3: 
102 C).(\lambda (_: T).(wf3 g c c3))) (\lambda (_: C).(\lambda (w0: T).(ty3 g c t 
103 w0))))).(ex3_2_ind C T (\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 
104 (Bind b0) t)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g c c3))) (\lambda (_: 
105 C).(\lambda (w0: T).(ty3 g c t w0))) (ex2 C (\lambda (d2: C).(getl (S n) c2 
106 (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2))) (\lambda (x0: 
107 C).(\lambda (x1: T).(\lambda (H8: (eq C c2 (CHead x0 (Bind b0) t))).(\lambda 
108 (H9: (wf3 g c x0)).(\lambda (_: (ty3 g c t x1)).(eq_ind_r C (CHead x0 (Bind 
109 b0) t) (\lambda (c0: C).(ex2 C (\lambda (d2: C).(getl (S n) c0 (CHead d2 
110 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)))) (let H_x0 \def (H c d1 v H5 g 
111 x0 H9 w H3) in (let H11 \def H_x0 in (ex2_ind C (\lambda (d2: C).(getl n x0 
112 (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)) (ex2 C (\lambda (d2: 
113 C).(getl (S n) (CHead x0 (Bind b0) t) (CHead d2 (Bind b) v))) (\lambda (d2: 
114 C).(wf3 g d1 d2))) (\lambda (x: C).(\lambda (H12: (getl n x0 (CHead x (Bind 
115 b) v))).(\lambda (H13: (wf3 g d1 x)).(ex_intro2 C (\lambda (d2: C).(getl (S 
116 n) (CHead x0 (Bind b0) t) (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 
117 d2)) x (getl_head (Bind b0) n x0 (CHead x (Bind b) v) H12 t) H13)))) H11))) 
118 c2 H8)))))) H7)) (\lambda (H7: (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 
119 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g c c3)) (\lambda (_: 
120 C).(\forall (w0: T).((ty3 g c t w0) \to False))))).(ex3_ind C (\lambda (c3: 
121 C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g c c3)) 
122 (\lambda (_: C).(\forall (w0: T).((ty3 g c t w0) \to False))) (ex2 C (\lambda 
123 (d2: C).(getl (S n) c2 (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 
124 d2))) (\lambda (x0: C).(\lambda (H8: (eq C c2 (CHead x0 (Bind Void) (TSort 
125 O)))).(\lambda (H9: (wf3 g c x0)).(\lambda (_: ((\forall (w0: T).((ty3 g c t 
126 w0) \to False)))).(eq_ind_r C (CHead x0 (Bind Void) (TSort O)) (\lambda (c0: 
127 C).(ex2 C (\lambda (d2: C).(getl (S n) c0 (CHead d2 (Bind b) v))) (\lambda 
128 (d2: C).(wf3 g d1 d2)))) (let H_x0 \def (H c d1 v H5 g x0 H9 w H3) in (let 
129 H11 \def H_x0 in (ex2_ind C (\lambda (d2: C).(getl n x0 (CHead d2 (Bind b) 
130 v))) (\lambda (d2: C).(wf3 g d1 d2)) (ex2 C (\lambda (d2: C).(getl (S n) 
131 (CHead x0 (Bind Void) (TSort O)) (CHead d2 (Bind b) v))) (\lambda (d2: 
132 C).(wf3 g d1 d2))) (\lambda (x: C).(\lambda (H12: (getl n x0 (CHead x (Bind 
133 b) v))).(\lambda (H13: (wf3 g d1 x)).(ex_intro2 C (\lambda (d2: C).(getl (S 
134 n) (CHead x0 (Bind Void) (TSort O)) (CHead d2 (Bind b) v))) (\lambda (d2: 
135 C).(wf3 g d1 d2)) x (getl_head (Bind Void) n x0 (CHead x (Bind b) v) H12 
136 (TSort O)) H13)))) H11))) c2 H8))))) H7)) H6)))))) (\lambda (f: F).(\lambda 
137 (H4: (wf3 g (CHead c (Flat f) t) c2)).(\lambda (H5: (getl (r (Flat f) n) c 
138 (CHead d1 (Bind b) v))).(let H_y \def (wf3_gen_flat1 g c c2 t f H4) in (H0 d1 
139 v H5 g c2 H_y w H3))))) k H2 (getl_gen_S k c (CHead d1 (Bind b) v) t n 
140 H1)))))))))))))) c1)))) i)).
141
142 lemma getl_wf3_trans:
143  \forall (i: nat).(\forall (c1: C).(\forall (d1: C).((getl i c1 d1) \to 
144 (\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) \to (ex2 C (\lambda (c2: 
145 C).(wf3 g c1 c2)) (\lambda (c2: C).(getl i c2 d2)))))))))
146 \def
147  \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: C).(\forall (d1: 
148 C).((getl n c1 d1) \to (\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) \to 
149 (ex2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(getl n c2 
150 d2)))))))))) (\lambda (c1: C).(\lambda (d1: C).(\lambda (H: (getl O c1 
151 d1)).(\lambda (g: G).(\lambda (d2: C).(\lambda (H0: (wf3 g d1 d2)).(let H_x 
152 \def (clear_wf3_trans c1 d1 (getl_gen_O c1 d1 H) g d2 H0) in (let H1 \def H_x 
153 in (ex2_ind C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(clear c2 d2)) 
154 (ex2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(getl O c2 d2))) 
155 (\lambda (x: C).(\lambda (H2: (wf3 g c1 x)).(\lambda (H3: (clear x 
156 d2)).(ex_intro2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(getl O c2 
157 d2)) x H2 (getl_intro O x d2 x (drop_refl x) H3))))) H1))))))))) (\lambda (n: 
158 nat).(\lambda (H: ((\forall (c1: C).(\forall (d1: C).((getl n c1 d1) \to 
159 (\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) \to (ex2 C (\lambda (c2: 
160 C).(wf3 g c1 c2)) (\lambda (c2: C).(getl n c2 d2))))))))))).(\lambda (c1: 
161 C).(C_ind (\lambda (c: C).(\forall (d1: C).((getl (S n) c d1) \to (\forall 
162 (g: G).(\forall (d2: C).((wf3 g d1 d2) \to (ex2 C (\lambda (c2: C).(wf3 g c 
163 c2)) (\lambda (c2: C).(getl (S n) c2 d2))))))))) (\lambda (n0: nat).(\lambda 
164 (d1: C).(\lambda (H0: (getl (S n) (CSort n0) d1)).(\lambda (g: G).(\lambda 
165 (d2: C).(\lambda (_: (wf3 g d1 d2)).(getl_gen_sort n0 (S n) d1 H0 (ex2 C 
166 (\lambda (c2: C).(wf3 g (CSort n0) c2)) (\lambda (c2: C).(getl (S n) c2 
167 d2)))))))))) (\lambda (c: C).(\lambda (H0: ((\forall (d1: C).((getl (S n) c 
168 d1) \to (\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) \to (ex2 C (\lambda 
169 (c2: C).(wf3 g c c2)) (\lambda (c2: C).(getl (S n) c2 d2)))))))))).(\lambda 
170 (k: K).(\lambda (t: T).(\lambda (d1: C).(\lambda (H1: (getl (S n) (CHead c k 
171 t) d1)).(\lambda (g: G).(\lambda (d2: C).(\lambda (H2: (wf3 g d1 d2)).(K_ind 
172 (\lambda (k0: K).((getl (r k0 n) c d1) \to (ex2 C (\lambda (c2: C).(wf3 g 
173 (CHead c k0 t) c2)) (\lambda (c2: C).(getl (S n) c2 d2))))) (\lambda (b: 
174 B).(\lambda (H3: (getl (r (Bind b) n) c d1)).(let H_x \def (H c d1 H3 g d2 
175 H2) in (let H4 \def H_x in (ex2_ind C (\lambda (c2: C).(wf3 g c c2)) (\lambda 
176 (c2: C).(getl n c2 d2)) (ex2 C (\lambda (c2: C).(wf3 g (CHead c (Bind b) t) 
177 c2)) (\lambda (c2: C).(getl (S n) c2 d2))) (\lambda (x: C).(\lambda (H5: (wf3 
178 g c x)).(\lambda (H6: (getl n x d2)).(let H_x0 \def (ty3_inference g c t) in 
179 (let H7 \def H_x0 in (or_ind (ex T (\lambda (t2: T).(ty3 g c t t2))) (\forall 
180 (t2: T).((ty3 g c t t2) \to False)) (ex2 C (\lambda (c2: C).(wf3 g (CHead c 
181 (Bind b) t) c2)) (\lambda (c2: C).(getl (S n) c2 d2))) (\lambda (H8: (ex T 
182 (\lambda (t2: T).(ty3 g c t t2)))).(ex_ind T (\lambda (t2: T).(ty3 g c t t2)) 
183 (ex2 C (\lambda (c2: C).(wf3 g (CHead c (Bind b) t) c2)) (\lambda (c2: 
184 C).(getl (S n) c2 d2))) (\lambda (x0: T).(\lambda (H9: (ty3 g c t 
185 x0)).(ex_intro2 C (\lambda (c2: C).(wf3 g (CHead c (Bind b) t) c2)) (\lambda 
186 (c2: C).(getl (S n) c2 d2)) (CHead x (Bind b) t) (wf3_bind g c x H5 t x0 H9 
187 b) (getl_head (Bind b) n x d2 H6 t)))) H8)) (\lambda (H8: ((\forall (t2: 
188 T).((ty3 g c t t2) \to False)))).(ex_intro2 C (\lambda (c2: C).(wf3 g (CHead 
189 c (Bind b) t) c2)) (\lambda (c2: C).(getl (S n) c2 d2)) (CHead x (Bind Void) 
190 (TSort O)) (wf3_void g c x H5 t H8 b) (getl_head (Bind Void) n x d2 H6 (TSort 
191 O)))) H7)))))) H4))))) (\lambda (f: F).(\lambda (H3: (getl (r (Flat f) n) c 
192 d1)).(let H_x \def (H0 d1 H3 g d2 H2) in (let H4 \def H_x in (ex2_ind C 
193 (\lambda (c2: C).(wf3 g c c2)) (\lambda (c2: C).(getl (S n) c2 d2)) (ex2 C 
194 (\lambda (c2: C).(wf3 g (CHead c (Flat f) t) c2)) (\lambda (c2: C).(getl (S 
195 n) c2 d2))) (\lambda (x: C).(\lambda (H5: (wf3 g c x)).(\lambda (H6: (getl (S 
196 n) x d2)).(ex_intro2 C (\lambda (c2: C).(wf3 g (CHead c (Flat f) t) c2)) 
197 (\lambda (c2: C).(getl (S n) c2 d2)) x (wf3_flat g c x H5 t f) H6)))) H4))))) 
198 k (getl_gen_S k c d1 t n H1))))))))))) c1)))) i).
199