1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/props".
19 include "nf2/defs.ma".
24 \forall (c: C).(\forall (n: nat).(nf2 c (TSort n)))
26 \lambda (c: C).(\lambda (n: nat).(\lambda (t2: T).(\lambda (H: (pr2 c (TSort
27 n) t2)).(eq_ind_r T (TSort n) (\lambda (t: T).(eq T (TSort n) t)) (refl_equal
28 T (TSort n)) t2 (pr2_gen_sort c t2 n H))))).
30 theorem nf2_csort_lref:
31 \forall (n: nat).(\forall (i: nat).(nf2 (CSort n) (TLRef i)))
33 \lambda (n: nat).(\lambda (i: nat).(\lambda (t2: T).(\lambda (H: (pr2 (CSort
34 n) (TLRef i) t2)).(let H0 \def (pr2_gen_lref (CSort n) t2 i H) in (or_ind (eq
35 T t2 (TLRef i)) (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i (CSort n)
36 (CHead d (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift (S
37 i) O u))))) (eq T (TLRef i) t2) (\lambda (H1: (eq T t2 (TLRef i))).(eq_ind_r
38 T (TLRef i) (\lambda (t: T).(eq T (TLRef i) t)) (refl_equal T (TLRef i)) t2
39 H1)) (\lambda (H1: (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i (CSort
40 n) (CHead d (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift
41 (S i) O u)))))).(ex2_2_ind C T (\lambda (d: C).(\lambda (u: T).(getl i (CSort
42 n) (CHead d (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift
43 (S i) O u)))) (eq T (TLRef i) t2) (\lambda (x0: C).(\lambda (x1: T).(\lambda
44 (H2: (getl i (CSort n) (CHead x0 (Bind Abbr) x1))).(\lambda (H3: (eq T t2
45 (lift (S i) O x1))).(eq_ind_r T (lift (S i) O x1) (\lambda (t: T).(eq T
46 (TLRef i) t)) (getl_gen_sort n i (CHead x0 (Bind Abbr) x1) H2 (eq T (TLRef i)
47 (lift (S i) O x1))) t2 H3))))) H1)) H0))))).
50 \forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (b: B).(\forall (v:
51 T).(\forall (t: T).((nf2 (CHead c (Bind b) v) t) \to (nf2 c (THead (Bind
54 \lambda (c: C).(\lambda (u: T).(\lambda (H: ((\forall (t2: T).((pr2 c u t2)
55 \to (eq T u t2))))).(\lambda (b: B).(\lambda (v: T).(\lambda (t: T).(\lambda
56 (H0: ((\forall (t2: T).((pr2 (CHead c (Bind b) v) t t2) \to (eq T t
57 t2))))).(\lambda (t2: T).(\lambda (H1: (pr2 c (THead (Bind Abst) u t)
58 t2)).(let H2 \def (pr2_gen_abst c u t t2 H1) in (ex3_2_ind T T (\lambda (u2:
59 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abst) u2 t3)))) (\lambda (u2:
60 T).(\lambda (_: T).(pr2 c u u2))) (\lambda (_: T).(\lambda (t3: T).(\forall
61 (b0: B).(\forall (u0: T).(pr2 (CHead c (Bind b0) u0) t t3))))) (eq T (THead
62 (Bind Abst) u t) t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H3: (eq T t2
63 (THead (Bind Abst) x0 x1))).(\lambda (H4: (pr2 c u x0)).(\lambda (H5:
64 ((\forall (b0: B).(\forall (u0: T).(pr2 (CHead c (Bind b0) u0) t
65 x1))))).(eq_ind_r T (THead (Bind Abst) x0 x1) (\lambda (t0: T).(eq T (THead
66 (Bind Abst) u t) t0)) (f_equal3 K T T T THead (Bind Abst) (Bind Abst) u x0 t
67 x1 (refl_equal K (Bind Abst)) (H x0 H4) (H0 x1 (H5 b v))) t2 H3))))))
70 theorem nf2_abst_shift:
71 \forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (t: T).((nf2 (CHead c
72 (Bind Abst) u) t) \to (nf2 c (THead (Bind Abst) u t))))))
74 \lambda (c: C).(\lambda (u: T).(\lambda (H: ((\forall (t2: T).((pr2 c u t2)
75 \to (eq T u t2))))).(\lambda (t: T).(\lambda (H0: ((\forall (t2: T).((pr2
76 (CHead c (Bind Abst) u) t t2) \to (eq T t t2))))).(\lambda (t2: T).(\lambda
77 (H1: (pr2 c (THead (Bind Abst) u t) t2)).(let H2 \def (pr2_gen_abst c u t t2
78 H1) in (ex3_2_ind T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
79 Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c u u2))) (\lambda (_:
80 T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind b)
81 u0) t t3))))) (eq T (THead (Bind Abst) u t) t2) (\lambda (x0: T).(\lambda
82 (x1: T).(\lambda (H3: (eq T t2 (THead (Bind Abst) x0 x1))).(\lambda (H4: (pr2
83 c u x0)).(\lambda (H5: ((\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind
84 b) u0) t x1))))).(eq_ind_r T (THead (Bind Abst) x0 x1) (\lambda (t0: T).(eq T
85 (THead (Bind Abst) u t) t0)) (f_equal3 K T T T THead (Bind Abst) (Bind Abst)
86 u x0 t x1 (refl_equal K (Bind Abst)) (H x0 H4) (H0 x1 (H5 Abst u))) t2
89 theorem nf2_appls_lref:
90 \forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (vs:
91 TList).((nfs2 c vs) \to (nf2 c (THeads (Flat Appl) vs (TLRef i)))))))
93 \lambda (c: C).(\lambda (i: nat).(\lambda (H: (nf2 c (TLRef i))).(\lambda
94 (vs: TList).(TList_ind (\lambda (t: TList).((nfs2 c t) \to (nf2 c (THeads
95 (Flat Appl) t (TLRef i))))) (\lambda (_: True).H) (\lambda (t: T).(\lambda
96 (t0: TList).(\lambda (H0: (((nfs2 c t0) \to (nf2 c (THeads (Flat Appl) t0
97 (TLRef i)))))).(\lambda (H1: (land (nf2 c t) (nfs2 c t0))).(let H2 \def H1 in
98 (and_ind (nf2 c t) (nfs2 c t0) (nf2 c (THead (Flat Appl) t (THeads (Flat
99 Appl) t0 (TLRef i)))) (\lambda (H3: (nf2 c t)).(\lambda (H4: (nfs2 c
100 t0)).(let H_y \def (H0 H4) in (\lambda (t2: T).(\lambda (H5: (pr2 c (THead
101 (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2)).(let H6 \def
102 (pr2_gen_appl c t (THeads (Flat Appl) t0 (TLRef i)) t2 H5) in (or3_ind (ex3_2
103 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3))))
104 (\lambda (u2: T).(\lambda (_: T).(pr2 c t u2))) (\lambda (_: T).(\lambda (t3:
105 T).(pr2 c (THeads (Flat Appl) t0 (TLRef i)) t3)))) (ex4_4 T T T T (\lambda
106 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T (THeads (Flat
107 Appl) t0 (TLRef i)) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda
108 (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2
109 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
110 T).(pr2 c t u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
111 (t3: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1
112 t3)))))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_:
113 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst))))))))
114 (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
115 (_: T).(\lambda (_: T).(eq T (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind
116 b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
117 (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind b) y2 (THead
118 (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_: B).(\lambda (_:
119 T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t
120 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
121 T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2))))))) (\lambda (b:
122 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda
123 (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2)))))))) (eq T (THead (Flat Appl) t
124 (THeads (Flat Appl) t0 (TLRef i))) t2) (\lambda (H7: (ex3_2 T T (\lambda (u2:
125 T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2:
126 T).(\lambda (_: T).(pr2 c t u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c
127 (THeads (Flat Appl) t0 (TLRef i)) t3))))).(ex3_2_ind T T (\lambda (u2:
128 T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2:
129 T).(\lambda (_: T).(pr2 c t u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c
130 (THeads (Flat Appl) t0 (TLRef i)) t3))) (eq T (THead (Flat Appl) t (THeads
131 (Flat Appl) t0 (TLRef i))) t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda
132 (H8: (eq T t2 (THead (Flat Appl) x0 x1))).(\lambda (H9: (pr2 c t
133 x0)).(\lambda (H10: (pr2 c (THeads (Flat Appl) t0 (TLRef i)) x1)).(eq_ind_r T
134 (THead (Flat Appl) x0 x1) (\lambda (t1: T).(eq T (THead (Flat Appl) t (THeads
135 (Flat Appl) t0 (TLRef i))) t1)) (let H11 \def (eq_ind_r T x1 (\lambda (t1:
136 T).(pr2 c (THeads (Flat Appl) t0 (TLRef i)) t1)) H10 (THeads (Flat Appl) t0
137 (TLRef i)) (H_y x1 H10)) in (eq_ind T (THeads (Flat Appl) t0 (TLRef i))
138 (\lambda (t1: T).(eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef
139 i))) (THead (Flat Appl) x0 t1))) (let H12 \def (eq_ind_r T x0 (\lambda (t1:
140 T).(pr2 c t t1)) H9 t (H3 x0 H9)) in (eq_ind T t (\lambda (t1: T).(eq T
141 (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) (THead (Flat Appl) t1
142 (THeads (Flat Appl) t0 (TLRef i))))) (refl_equal T (THead (Flat Appl) t
143 (THeads (Flat Appl) t0 (TLRef i)))) x0 (H3 x0 H9))) x1 (H_y x1 H10))) t2
144 H8)))))) H7)) (\lambda (H7: (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1:
145 T).(\lambda (_: T).(\lambda (_: T).(eq T (THeads (Flat Appl) t0 (TLRef i))
146 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
147 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_:
148 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t u2))))) (\lambda
149 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b:
150 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t3))))))))).(ex4_4_ind T T T
151 T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
152 (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
153 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
154 Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
155 (_: T).(pr2 c t u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
156 T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u)
157 z1 t3))))))) (eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i)))
158 t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3:
159 T).(\lambda (H8: (eq T (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst)
160 x0 x1))).(\lambda (H9: (eq T t2 (THead (Bind Abbr) x2 x3))).(\lambda (_: (pr2
161 c t x2)).(\lambda (_: ((\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b)
162 u) x1 x3))))).(eq_ind_r T (THead (Bind Abbr) x2 x3) (\lambda (t1: T).(eq T
163 (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t1)) (TList_ind
164 (\lambda (t1: TList).((nf2 c (THeads (Flat Appl) t1 (TLRef i))) \to ((eq T
165 (THeads (Flat Appl) t1 (TLRef i)) (THead (Bind Abst) x0 x1)) \to (eq T (THead
166 (Flat Appl) t (THeads (Flat Appl) t1 (TLRef i))) (THead (Bind Abbr) x2
167 x3))))) (\lambda (_: (nf2 c (THeads (Flat Appl) TNil (TLRef i)))).(\lambda
168 (H13: (eq T (THeads (Flat Appl) TNil (TLRef i)) (THead (Bind Abst) x0
169 x1))).(let H14 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T
170 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
171 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Bind Abst) x0
172 x1) H13) in (False_ind (eq T (THead (Flat Appl) t (THeads (Flat Appl) TNil
173 (TLRef i))) (THead (Bind Abbr) x2 x3)) H14)))) (\lambda (t1: T).(\lambda (t3:
174 TList).(\lambda (_: (((nf2 c (THeads (Flat Appl) t3 (TLRef i))) \to ((eq T
175 (THeads (Flat Appl) t3 (TLRef i)) (THead (Bind Abst) x0 x1)) \to (eq T (THead
176 (Flat Appl) t (THeads (Flat Appl) t3 (TLRef i))) (THead (Bind Abbr) x2
177 x3)))))).(\lambda (_: (nf2 c (THeads (Flat Appl) (TCons t1 t3) (TLRef
178 i)))).(\lambda (H13: (eq T (THeads (Flat Appl) (TCons t1 t3) (TLRef i))
179 (THead (Bind Abst) x0 x1))).(let H14 \def (eq_ind T (THead (Flat Appl) t1
180 (THeads (Flat Appl) t3 (TLRef i))) (\lambda (ee: T).(match ee in T return
181 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
182 \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda
183 (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
184 True])])) I (THead (Bind Abst) x0 x1) H13) in (False_ind (eq T (THead (Flat
185 Appl) t (THeads (Flat Appl) (TCons t1 t3) (TLRef i))) (THead (Bind Abbr) x2
186 x3)) H14))))))) t0 H_y H8) t2 H9))))))))) H7)) (\lambda (H7: (ex6_6 B T T T T
187 T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
188 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
189 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq
190 T (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind b) y1 z1)))))))) (\lambda
191 (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2:
192 T).(\lambda (y2: T).(eq T t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S
193 O) O u2) z2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda
194 (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t u2))))))) (\lambda (_:
195 B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
196 (y2: T).(pr2 c y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
197 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b)
198 y2) z1 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda (_:
199 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B
200 b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
201 T).(\lambda (_: T).(\lambda (_: T).(eq T (THeads (Flat Appl) t0 (TLRef i))
202 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
203 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind
204 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
205 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
206 (_: T).(pr2 c t u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
207 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
208 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
209 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))) (eq T (THead
210 (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2) (\lambda (x0:
211 B).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4:
212 T).(\lambda (x5: T).(\lambda (_: (not (eq B x0 Abst))).(\lambda (H9: (eq T
213 (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind x0) x1 x2))).(\lambda (H10:
214 (eq T t2 (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4)
215 x3)))).(\lambda (_: (pr2 c t x4)).(\lambda (_: (pr2 c x1 x5)).(\lambda (_:
216 (pr2 (CHead c (Bind x0) x5) x2 x3)).(eq_ind_r T (THead (Bind x0) x5 (THead
217 (Flat Appl) (lift (S O) O x4) x3)) (\lambda (t1: T).(eq T (THead (Flat Appl)
218 t (THeads (Flat Appl) t0 (TLRef i))) t1)) (TList_ind (\lambda (t1:
219 TList).((nf2 c (THeads (Flat Appl) t1 (TLRef i))) \to ((eq T (THeads (Flat
220 Appl) t1 (TLRef i)) (THead (Bind x0) x1 x2)) \to (eq T (THead (Flat Appl) t
221 (THeads (Flat Appl) t1 (TLRef i))) (THead (Bind x0) x5 (THead (Flat Appl)
222 (lift (S O) O x4) x3)))))) (\lambda (_: (nf2 c (THeads (Flat Appl) TNil
223 (TLRef i)))).(\lambda (H15: (eq T (THeads (Flat Appl) TNil (TLRef i)) (THead
224 (Bind x0) x1 x2))).(let H16 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match
225 ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False |
226 (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead
227 (Bind x0) x1 x2) H15) in (False_ind (eq T (THead (Flat Appl) t (THeads (Flat
228 Appl) TNil (TLRef i))) (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O
229 x4) x3))) H16)))) (\lambda (t1: T).(\lambda (t3: TList).(\lambda (_: (((nf2 c
230 (THeads (Flat Appl) t3 (TLRef i))) \to ((eq T (THeads (Flat Appl) t3 (TLRef
231 i)) (THead (Bind x0) x1 x2)) \to (eq T (THead (Flat Appl) t (THeads (Flat
232 Appl) t3 (TLRef i))) (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4)
233 x3))))))).(\lambda (_: (nf2 c (THeads (Flat Appl) (TCons t1 t3) (TLRef
234 i)))).(\lambda (H15: (eq T (THeads (Flat Appl) (TCons t1 t3) (TLRef i))
235 (THead (Bind x0) x1 x2))).(let H16 \def (eq_ind T (THead (Flat Appl) t1
236 (THeads (Flat Appl) t3 (TLRef i))) (\lambda (ee: T).(match ee in T return
237 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
238 \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda
239 (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
240 True])])) I (THead (Bind x0) x1 x2) H15) in (False_ind (eq T (THead (Flat
241 Appl) t (THeads (Flat Appl) (TCons t1 t3) (TLRef i))) (THead (Bind x0) x5
242 (THead (Flat Appl) (lift (S O) O x4) x3))) H16))))))) t0 H_y H9) t2
243 H10))))))))))))) H7)) H6))))))) H2)))))) vs)))).
245 theorem nf2_appl_lref:
246 \forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (i: nat).((nf2 c
247 (TLRef i)) \to (nf2 c (THead (Flat Appl) u (TLRef i)))))))
249 \lambda (c: C).(\lambda (u: T).(\lambda (H: (nf2 c u)).(\lambda (i:
250 nat).(\lambda (H0: (nf2 c (TLRef i))).(let H_y \def (nf2_appls_lref c i H0
251 (TCons u TNil)) in (H_y (conj (nf2 c u) True H I))))))).
253 theorem nf2_lref_abst:
254 \forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (i: nat).((getl i c
255 (CHead e (Bind Abst) u)) \to (nf2 c (TLRef i))))))
257 \lambda (c: C).(\lambda (e: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
258 (H: (getl i c (CHead e (Bind Abst) u))).(\lambda (t2: T).(\lambda (H0: (pr2 c
259 (TLRef i) t2)).(let H1 \def (pr2_gen_lref c t2 i H0) in (or_ind (eq T t2
260 (TLRef i)) (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i c (CHead d
261 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(eq T t2 (lift (S i) O
262 u0))))) (eq T (TLRef i) t2) (\lambda (H2: (eq T t2 (TLRef i))).(eq_ind_r T
263 (TLRef i) (\lambda (t: T).(eq T (TLRef i) t)) (refl_equal T (TLRef i)) t2
264 H2)) (\lambda (H2: (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i c
265 (CHead d (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(eq T t2 (lift
266 (S i) O u0)))))).(ex2_2_ind C T (\lambda (d: C).(\lambda (u0: T).(getl i c
267 (CHead d (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(eq T t2 (lift
268 (S i) O u0)))) (eq T (TLRef i) t2) (\lambda (x0: C).(\lambda (x1: T).(\lambda
269 (H3: (getl i c (CHead x0 (Bind Abbr) x1))).(\lambda (H4: (eq T t2 (lift (S i)
270 O x1))).(eq_ind_r T (lift (S i) O x1) (\lambda (t: T).(eq T (TLRef i) t))
271 (let H5 \def (eq_ind C (CHead e (Bind Abst) u) (\lambda (c0: C).(getl i c
272 c0)) H (CHead x0 (Bind Abbr) x1) (getl_mono c (CHead e (Bind Abst) u) i H
273 (CHead x0 (Bind Abbr) x1) H3)) in (let H6 \def (eq_ind C (CHead e (Bind Abst)
274 u) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort
275 _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return
276 (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return
277 (\lambda (_: B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow True |
278 Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead x0 (Bind
279 Abbr) x1) (getl_mono c (CHead e (Bind Abst) u) i H (CHead x0 (Bind Abbr) x1)
280 H3)) in (False_ind (eq T (TLRef i) (lift (S i) O x1)) H6))) t2 H4))))) H2))
284 \forall (d: C).(\forall (t: T).((nf2 d t) \to (\forall (c: C).(\forall (h:
285 nat).(\forall (i: nat).((drop h i c d) \to (nf2 c (lift h i t))))))))
287 \lambda (d: C).(\lambda (t: T).(\lambda (H: ((\forall (t2: T).((pr2 d t t2)
288 \to (eq T t t2))))).(\lambda (c: C).(\lambda (h: nat).(\lambda (i:
289 nat).(\lambda (H0: (drop h i c d)).(\lambda (t2: T).(\lambda (H1: (pr2 c
290 (lift h i t) t2)).(let H2 \def (pr2_gen_lift c t t2 h i H1 d H0) in (ex2_ind
291 T (\lambda (t3: T).(eq T t2 (lift h i t3))) (\lambda (t3: T).(pr2 d t t3))
292 (eq T (lift h i t) t2) (\lambda (x: T).(\lambda (H3: (eq T t2 (lift h i
293 x))).(\lambda (H4: (pr2 d t x)).(eq_ind_r T (lift h i x) (\lambda (t0: T).(eq
294 T (lift h i t) t0)) (let H_y \def (H x H4) in (let H5 \def (eq_ind_r T x
295 (\lambda (t0: T).(pr2 d t t0)) H4 t H_y) in (eq_ind T t (\lambda (t0: T).(eq
296 T (lift h i t) (lift h i t0))) (refl_equal T (lift h i t)) x H_y))) t2 H3))))