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 include "iso/defs.ma".
19 include "tlist/defs.ma".
21 theorem iso_flats_lref_bind_false:
22 \forall (f: F).(\forall (b: B).(\forall (i: nat).(\forall (v: T).(\forall
23 (t: T).(\forall (vs: TList).((iso (THeads (Flat f) vs (TLRef i)) (THead (Bind
24 b) v t)) \to (\forall (P: Prop).P)))))))
26 \lambda (f: F).(\lambda (b: B).(\lambda (i: nat).(\lambda (v: T).(\lambda
27 (t: T).(\lambda (vs: TList).(TList_ind (\lambda (t0: TList).((iso (THeads
28 (Flat f) t0 (TLRef i)) (THead (Bind b) v t)) \to (\forall (P: Prop).P)))
29 (\lambda (H: (iso (TLRef i) (THead (Bind b) v t))).(\lambda (P: Prop).(let H0
30 \def (match H in iso return (\lambda (t0: T).(\lambda (t1: T).(\lambda (_:
31 (iso t0 t1)).((eq T t0 (TLRef i)) \to ((eq T t1 (THead (Bind b) v t)) \to
32 P))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq T (TSort n1)
33 (TLRef i))).(\lambda (H1: (eq T (TSort n2) (THead (Bind b) v t))).((let H2
34 \def (eq_ind T (TSort n1) (\lambda (e: T).(match e in T return (\lambda (_:
35 T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
36 (THead _ _ _) \Rightarrow False])) I (TLRef i) H0) in (False_ind ((eq T
37 (TSort n2) (THead (Bind b) v t)) \to P) H2)) H1))) | (iso_lref i1 i2)
38 \Rightarrow (\lambda (H0: (eq T (TLRef i1) (TLRef i))).(\lambda (H1: (eq T
39 (TLRef i2) (THead (Bind b) v t))).((let H2 \def (f_equal T nat (\lambda (e:
40 T).(match e in T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow i1 |
41 (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i1])) (TLRef i1) (TLRef
42 i) H0) in (eq_ind nat i (\lambda (_: nat).((eq T (TLRef i2) (THead (Bind b) v
43 t)) \to P)) (\lambda (H3: (eq T (TLRef i2) (THead (Bind b) v t))).(let H4
44 \def (eq_ind T (TLRef i2) (\lambda (e: T).(match e in T return (\lambda (_:
45 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
46 (THead _ _ _) \Rightarrow False])) I (THead (Bind b) v t) H3) in (False_ind P
47 H4))) i1 (sym_eq nat i1 i H2))) H1))) | (iso_head v1 v2 t1 t2 k) \Rightarrow
48 (\lambda (H0: (eq T (THead k v1 t1) (TLRef i))).(\lambda (H1: (eq T (THead k
49 v2 t2) (THead (Bind b) v t))).((let H2 \def (eq_ind T (THead k v1 t1)
50 (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
51 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
52 True])) I (TLRef i) H0) in (False_ind ((eq T (THead k v2 t2) (THead (Bind b)
53 v t)) \to P) H2)) H1)))]) in (H0 (refl_equal T (TLRef i)) (refl_equal T
54 (THead (Bind b) v t)))))) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (_:
55 (((iso (THeads (Flat f) t1 (TLRef i)) (THead (Bind b) v t)) \to (\forall (P:
56 Prop).P)))).(\lambda (H0: (iso (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef
57 i))) (THead (Bind b) v t))).(\lambda (P: Prop).(let H1 \def (match H0 in iso
58 return (\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (iso t2 t3)).((eq T t2
59 (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i)))) \to ((eq T t3 (THead
60 (Bind b) v t)) \to P))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H1:
61 (eq T (TSort n1) (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef
62 i))))).(\lambda (H2: (eq T (TSort n2) (THead (Bind b) v t))).((let H3 \def
63 (eq_ind T (TSort n1) (\lambda (e: T).(match e in T return (\lambda (_:
64 T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
65 (THead _ _ _) \Rightarrow False])) I (THead (Flat f) t0 (THeads (Flat f) t1
66 (TLRef i))) H1) in (False_ind ((eq T (TSort n2) (THead (Bind b) v t)) \to P)
67 H3)) H2))) | (iso_lref i1 i2) \Rightarrow (\lambda (H1: (eq T (TLRef i1)
68 (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i))))).(\lambda (H2: (eq T
69 (TLRef i2) (THead (Bind b) v t))).((let H3 \def (eq_ind T (TLRef i1) (\lambda
70 (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
71 False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
72 (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i))) H1) in (False_ind ((eq T
73 (TLRef i2) (THead (Bind b) v t)) \to P) H3)) H2))) | (iso_head v1 v2 t2 t3 k)
74 \Rightarrow (\lambda (H1: (eq T (THead k v1 t2) (THead (Flat f) t0 (THeads
75 (Flat f) t1 (TLRef i))))).(\lambda (H2: (eq T (THead k v2 t3) (THead (Bind b)
76 v t))).((let H3 \def (f_equal T T (\lambda (e: T).(match e in T return
77 (\lambda (_: T).T) with [(TSort _) \Rightarrow t2 | (TLRef _) \Rightarrow t2
78 | (THead _ _ t4) \Rightarrow t4])) (THead k v1 t2) (THead (Flat f) t0 (THeads
79 (Flat f) t1 (TLRef i))) H1) in ((let H4 \def (f_equal T T (\lambda (e:
80 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v1 |
81 (TLRef _) \Rightarrow v1 | (THead _ t4 _) \Rightarrow t4])) (THead k v1 t2)
82 (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i))) H1) in ((let H5 \def
83 (f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with
84 [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _)
85 \Rightarrow k0])) (THead k v1 t2) (THead (Flat f) t0 (THeads (Flat f) t1
86 (TLRef i))) H1) in (eq_ind K (Flat f) (\lambda (k0: K).((eq T v1 t0) \to ((eq
87 T t2 (THeads (Flat f) t1 (TLRef i))) \to ((eq T (THead k0 v2 t3) (THead (Bind
88 b) v t)) \to P)))) (\lambda (H6: (eq T v1 t0)).(eq_ind T t0 (\lambda (_:
89 T).((eq T t2 (THeads (Flat f) t1 (TLRef i))) \to ((eq T (THead (Flat f) v2
90 t3) (THead (Bind b) v t)) \to P))) (\lambda (H7: (eq T t2 (THeads (Flat f) t1
91 (TLRef i)))).(eq_ind T (THeads (Flat f) t1 (TLRef i)) (\lambda (_: T).((eq T
92 (THead (Flat f) v2 t3) (THead (Bind b) v t)) \to P)) (\lambda (H8: (eq T
93 (THead (Flat f) v2 t3) (THead (Bind b) v t))).(let H9 \def (eq_ind T (THead
94 (Flat f) v2 t3) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop)
95 with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k0 _
96 _) \Rightarrow (match k0 in K return (\lambda (_: K).Prop) with [(Bind _)
97 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind b) v t) H8)
98 in (False_ind P H9))) t2 (sym_eq T t2 (THeads (Flat f) t1 (TLRef i)) H7))) v1
99 (sym_eq T v1 t0 H6))) k (sym_eq K k (Flat f) H5))) H4)) H3)) H2)))]) in (H1
100 (refl_equal T (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i)))) (refl_equal
101 T (THead (Bind b) v t))))))))) vs)))))).
103 theorem iso_flats_flat_bind_false:
104 \forall (f1: F).(\forall (f2: F).(\forall (b: B).(\forall (v: T).(\forall
105 (v2: T).(\forall (t: T).(\forall (t2: T).(\forall (vs: TList).((iso (THeads
106 (Flat f1) vs (THead (Flat f2) v2 t2)) (THead (Bind b) v t)) \to (\forall (P:
109 \lambda (f1: F).(\lambda (f2: F).(\lambda (b: B).(\lambda (v: T).(\lambda
110 (v2: T).(\lambda (t: T).(\lambda (t2: T).(\lambda (vs: TList).(TList_ind
111 (\lambda (t0: TList).((iso (THeads (Flat f1) t0 (THead (Flat f2) v2 t2))
112 (THead (Bind b) v t)) \to (\forall (P: Prop).P))) (\lambda (H: (iso (THead
113 (Flat f2) v2 t2) (THead (Bind b) v t))).(\lambda (P: Prop).(let H0 \def
114 (match H in iso return (\lambda (t0: T).(\lambda (t1: T).(\lambda (_: (iso t0
115 t1)).((eq T t0 (THead (Flat f2) v2 t2)) \to ((eq T t1 (THead (Bind b) v t))
116 \to P))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq T (TSort n1)
117 (THead (Flat f2) v2 t2))).(\lambda (H1: (eq T (TSort n2) (THead (Bind b) v
118 t))).((let H2 \def (eq_ind T (TSort n1) (\lambda (e: T).(match e in T return
119 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _)
120 \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead (Flat f2) v2
121 t2) H0) in (False_ind ((eq T (TSort n2) (THead (Bind b) v t)) \to P) H2))
122 H1))) | (iso_lref i1 i2) \Rightarrow (\lambda (H0: (eq T (TLRef i1) (THead
123 (Flat f2) v2 t2))).(\lambda (H1: (eq T (TLRef i2) (THead (Bind b) v
124 t))).((let H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T return
125 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
126 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Flat f2) v2
127 t2) H0) in (False_ind ((eq T (TLRef i2) (THead (Bind b) v t)) \to P) H2))
128 H1))) | (iso_head v1 v0 t1 t0 k) \Rightarrow (\lambda (H0: (eq T (THead k v1
129 t1) (THead (Flat f2) v2 t2))).(\lambda (H1: (eq T (THead k v0 t0) (THead
130 (Bind b) v t))).((let H2 \def (f_equal T T (\lambda (e: T).(match e in T
131 return (\lambda (_: T).T) with [(TSort _) \Rightarrow t1 | (TLRef _)
132 \Rightarrow t1 | (THead _ _ t3) \Rightarrow t3])) (THead k v1 t1) (THead
133 (Flat f2) v2 t2) H0) in ((let H3 \def (f_equal T T (\lambda (e: T).(match e
134 in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v1 | (TLRef _)
135 \Rightarrow v1 | (THead _ t3 _) \Rightarrow t3])) (THead k v1 t1) (THead
136 (Flat f2) v2 t2) H0) in ((let H4 \def (f_equal T K (\lambda (e: T).(match e
137 in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _)
138 \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k v1 t1) (THead (Flat
139 f2) v2 t2) H0) in (eq_ind K (Flat f2) (\lambda (k0: K).((eq T v1 v2) \to ((eq
140 T t1 t2) \to ((eq T (THead k0 v0 t0) (THead (Bind b) v t)) \to P)))) (\lambda
141 (H5: (eq T v1 v2)).(eq_ind T v2 (\lambda (_: T).((eq T t1 t2) \to ((eq T
142 (THead (Flat f2) v0 t0) (THead (Bind b) v t)) \to P))) (\lambda (H6: (eq T t1
143 t2)).(eq_ind T t2 (\lambda (_: T).((eq T (THead (Flat f2) v0 t0) (THead (Bind
144 b) v t)) \to P)) (\lambda (H7: (eq T (THead (Flat f2) v0 t0) (THead (Bind b)
145 v t))).(let H8 \def (eq_ind T (THead (Flat f2) v0 t0) (\lambda (e: T).(match
146 e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False |
147 (TLRef _) \Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in K
148 return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _)
149 \Rightarrow True])])) I (THead (Bind b) v t) H7) in (False_ind P H8))) t1
150 (sym_eq T t1 t2 H6))) v1 (sym_eq T v1 v2 H5))) k (sym_eq K k (Flat f2) H4)))
151 H3)) H2)) H1)))]) in (H0 (refl_equal T (THead (Flat f2) v2 t2)) (refl_equal T
152 (THead (Bind b) v t)))))) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (_:
153 (((iso (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)) (THead (Bind b) v t))
154 \to (\forall (P: Prop).P)))).(\lambda (H0: (iso (THead (Flat f1) t0 (THeads
155 (Flat f1) t1 (THead (Flat f2) v2 t2))) (THead (Bind b) v t))).(\lambda (P:
156 Prop).(let H1 \def (match H0 in iso return (\lambda (t3: T).(\lambda (t4:
157 T).(\lambda (_: (iso t3 t4)).((eq T t3 (THead (Flat f1) t0 (THeads (Flat f1)
158 t1 (THead (Flat f2) v2 t2)))) \to ((eq T t4 (THead (Bind b) v t)) \to P)))))
159 with [(iso_sort n1 n2) \Rightarrow (\lambda (H1: (eq T (TSort n1) (THead
160 (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))))).(\lambda (H2:
161 (eq T (TSort n2) (THead (Bind b) v t))).((let H3 \def (eq_ind T (TSort n1)
162 (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
163 \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
164 False])) I (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)))
165 H1) in (False_ind ((eq T (TSort n2) (THead (Bind b) v t)) \to P) H3)) H2))) |
166 (iso_lref i1 i2) \Rightarrow (\lambda (H1: (eq T (TLRef i1) (THead (Flat f1)
167 t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))))).(\lambda (H2: (eq T
168 (TLRef i2) (THead (Bind b) v t))).((let H3 \def (eq_ind T (TLRef i1) (\lambda
169 (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
170 False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
171 (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) H1) in
172 (False_ind ((eq T (TLRef i2) (THead (Bind b) v t)) \to P) H3)) H2))) |
173 (iso_head v1 v0 t3 t4 k) \Rightarrow (\lambda (H1: (eq T (THead k v1 t3)
174 (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))))).(\lambda
175 (H2: (eq T (THead k v0 t4) (THead (Bind b) v t))).((let H3 \def (f_equal T T
176 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
177 \Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ _ t5) \Rightarrow t5]))
178 (THead k v1 t3) (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2
179 t2))) H1) in ((let H4 \def (f_equal T T (\lambda (e: T).(match e in T return
180 (\lambda (_: T).T) with [(TSort _) \Rightarrow v1 | (TLRef _) \Rightarrow v1
181 | (THead _ t5 _) \Rightarrow t5])) (THead k v1 t3) (THead (Flat f1) t0
182 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) H1) in ((let H5 \def (f_equal
183 T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with [(TSort _)
184 \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _) \Rightarrow k0]))
185 (THead k v1 t3) (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2
186 t2))) H1) in (eq_ind K (Flat f1) (\lambda (k0: K).((eq T v1 t0) \to ((eq T t3
187 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) \to ((eq T (THead k0 v0 t4)
188 (THead (Bind b) v t)) \to P)))) (\lambda (H6: (eq T v1 t0)).(eq_ind T t0
189 (\lambda (_: T).((eq T t3 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) \to
190 ((eq T (THead (Flat f1) v0 t4) (THead (Bind b) v t)) \to P))) (\lambda (H7:
191 (eq T t3 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)))).(eq_ind T (THeads
192 (Flat f1) t1 (THead (Flat f2) v2 t2)) (\lambda (_: T).((eq T (THead (Flat f1)
193 v0 t4) (THead (Bind b) v t)) \to P)) (\lambda (H8: (eq T (THead (Flat f1) v0
194 t4) (THead (Bind b) v t))).(let H9 \def (eq_ind T (THead (Flat f1) v0 t4)
195 (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
196 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k0 _ _) \Rightarrow
197 (match k0 in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False
198 | (Flat _) \Rightarrow True])])) I (THead (Bind b) v t) H8) in (False_ind P
199 H9))) t3 (sym_eq T t3 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)) H7))) v1
200 (sym_eq T v1 t0 H6))) k (sym_eq K k (Flat f1) H5))) H4)) H3)) H2)))]) in (H1
201 (refl_equal T (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2
202 t2)))) (refl_equal T (THead (Bind b) v t))))))))) vs)))))))).
204 theorem iso_gen_sort:
205 \forall (u2: T).(\forall (n1: nat).((iso (TSort n1) u2) \to (ex nat (\lambda
206 (n2: nat).(eq T u2 (TSort n2))))))
208 \lambda (u2: T).(\lambda (n1: nat).(\lambda (H: (iso (TSort n1) u2)).(let H0
209 \def (match H in iso return (\lambda (t: T).(\lambda (t0: T).(\lambda (_:
210 (iso t t0)).((eq T t (TSort n1)) \to ((eq T t0 u2) \to (ex nat (\lambda (n2:
211 nat).(eq T u2 (TSort n2))))))))) with [(iso_sort n0 n2) \Rightarrow (\lambda
212 (H0: (eq T (TSort n0) (TSort n1))).(\lambda (H1: (eq T (TSort n2) u2)).((let
213 H2 \def (f_equal T nat (\lambda (e: T).(match e in T return (\lambda (_:
214 T).nat) with [(TSort n) \Rightarrow n | (TLRef _) \Rightarrow n0 | (THead _ _
215 _) \Rightarrow n0])) (TSort n0) (TSort n1) H0) in (eq_ind nat n1 (\lambda (_:
216 nat).((eq T (TSort n2) u2) \to (ex nat (\lambda (n3: nat).(eq T u2 (TSort
217 n3)))))) (\lambda (H3: (eq T (TSort n2) u2)).(eq_ind T (TSort n2) (\lambda
218 (t: T).(ex nat (\lambda (n3: nat).(eq T t (TSort n3))))) (ex_intro nat
219 (\lambda (n3: nat).(eq T (TSort n2) (TSort n3))) n2 (refl_equal T (TSort
220 n2))) u2 H3)) n0 (sym_eq nat n0 n1 H2))) H1))) | (iso_lref i1 i2) \Rightarrow
221 (\lambda (H0: (eq T (TLRef i1) (TSort n1))).(\lambda (H1: (eq T (TLRef i2)
222 u2)).((let H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T return
223 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
224 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n1) H0) in
225 (False_ind ((eq T (TLRef i2) u2) \to (ex nat (\lambda (n2: nat).(eq T u2
226 (TSort n2))))) H2)) H1))) | (iso_head v1 v2 t1 t2 k) \Rightarrow (\lambda
227 (H0: (eq T (THead k v1 t1) (TSort n1))).(\lambda (H1: (eq T (THead k v2 t2)
228 u2)).((let H2 \def (eq_ind T (THead k v1 t1) (\lambda (e: T).(match e in T
229 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
230 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n1) H0) in
231 (False_ind ((eq T (THead k v2 t2) u2) \to (ex nat (\lambda (n2: nat).(eq T u2
232 (TSort n2))))) H2)) H1)))]) in (H0 (refl_equal T (TSort n1)) (refl_equal T
235 theorem iso_gen_lref:
236 \forall (u2: T).(\forall (n1: nat).((iso (TLRef n1) u2) \to (ex nat (\lambda
237 (n2: nat).(eq T u2 (TLRef n2))))))
239 \lambda (u2: T).(\lambda (n1: nat).(\lambda (H: (iso (TLRef n1) u2)).(let H0
240 \def (match H in iso return (\lambda (t: T).(\lambda (t0: T).(\lambda (_:
241 (iso t t0)).((eq T t (TLRef n1)) \to ((eq T t0 u2) \to (ex nat (\lambda (n2:
242 nat).(eq T u2 (TLRef n2))))))))) with [(iso_sort n0 n2) \Rightarrow (\lambda
243 (H0: (eq T (TSort n0) (TLRef n1))).(\lambda (H1: (eq T (TSort n2) u2)).((let
244 H2 \def (eq_ind T (TSort n0) (\lambda (e: T).(match e in T return (\lambda
245 (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
246 (THead _ _ _) \Rightarrow False])) I (TLRef n1) H0) in (False_ind ((eq T
247 (TSort n2) u2) \to (ex nat (\lambda (n3: nat).(eq T u2 (TLRef n3))))) H2))
248 H1))) | (iso_lref i1 i2) \Rightarrow (\lambda (H0: (eq T (TLRef i1) (TLRef
249 n1))).(\lambda (H1: (eq T (TLRef i2) u2)).((let H2 \def (f_equal T nat
250 (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _)
251 \Rightarrow i1 | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i1]))
252 (TLRef i1) (TLRef n1) H0) in (eq_ind nat n1 (\lambda (_: nat).((eq T (TLRef
253 i2) u2) \to (ex nat (\lambda (n2: nat).(eq T u2 (TLRef n2)))))) (\lambda (H3:
254 (eq T (TLRef i2) u2)).(eq_ind T (TLRef i2) (\lambda (t: T).(ex nat (\lambda
255 (n2: nat).(eq T t (TLRef n2))))) (ex_intro nat (\lambda (n2: nat).(eq T
256 (TLRef i2) (TLRef n2))) i2 (refl_equal T (TLRef i2))) u2 H3)) i1 (sym_eq nat
257 i1 n1 H2))) H1))) | (iso_head v1 v2 t1 t2 k) \Rightarrow (\lambda (H0: (eq T
258 (THead k v1 t1) (TLRef n1))).(\lambda (H1: (eq T (THead k v2 t2) u2)).((let
259 H2 \def (eq_ind T (THead k v1 t1) (\lambda (e: T).(match e in T return
260 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
261 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n1) H0) in
262 (False_ind ((eq T (THead k v2 t2) u2) \to (ex nat (\lambda (n2: nat).(eq T u2
263 (TLRef n2))))) H2)) H1)))]) in (H0 (refl_equal T (TLRef n1)) (refl_equal T
266 theorem iso_gen_head:
267 \forall (k: K).(\forall (v1: T).(\forall (t1: T).(\forall (u2: T).((iso
268 (THead k v1 t1) u2) \to (ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T u2
269 (THead k v2 t2)))))))))
271 \lambda (k: K).(\lambda (v1: T).(\lambda (t1: T).(\lambda (u2: T).(\lambda
272 (H: (iso (THead k v1 t1) u2)).(let H0 \def (match H in iso return (\lambda
273 (t: T).(\lambda (t0: T).(\lambda (_: (iso t t0)).((eq T t (THead k v1 t1))
274 \to ((eq T t0 u2) \to (ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T u2
275 (THead k v2 t2)))))))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq
276 T (TSort n1) (THead k v1 t1))).(\lambda (H1: (eq T (TSort n2) u2)).((let H2
277 \def (eq_ind T (TSort n1) (\lambda (e: T).(match e in T return (\lambda (_:
278 T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
279 (THead _ _ _) \Rightarrow False])) I (THead k v1 t1) H0) in (False_ind ((eq T
280 (TSort n2) u2) \to (ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T u2
281 (THead k v2 t2)))))) H2)) H1))) | (iso_lref i1 i2) \Rightarrow (\lambda (H0:
282 (eq T (TLRef i1) (THead k v1 t1))).(\lambda (H1: (eq T (TLRef i2) u2)).((let
283 H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T return (\lambda
284 (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
285 (THead _ _ _) \Rightarrow False])) I (THead k v1 t1) H0) in (False_ind ((eq T
286 (TLRef i2) u2) \to (ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T u2
287 (THead k v2 t2)))))) H2)) H1))) | (iso_head v0 v2 t0 t2 k0) \Rightarrow
288 (\lambda (H0: (eq T (THead k0 v0 t0) (THead k v1 t1))).(\lambda (H1: (eq T
289 (THead k0 v2 t2) u2)).((let H2 \def (f_equal T T (\lambda (e: T).(match e in
290 T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _)
291 \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead k0 v0 t0) (THead k v1
292 t1) H0) in ((let H3 \def (f_equal T T (\lambda (e: T).(match e in T return
293 (\lambda (_: T).T) with [(TSort _) \Rightarrow v0 | (TLRef _) \Rightarrow v0
294 | (THead _ t _) \Rightarrow t])) (THead k0 v0 t0) (THead k v1 t1) H0) in
295 ((let H4 \def (f_equal T K (\lambda (e: T).(match e in T return (\lambda (_:
296 T).K) with [(TSort _) \Rightarrow k0 | (TLRef _) \Rightarrow k0 | (THead k1 _
297 _) \Rightarrow k1])) (THead k0 v0 t0) (THead k v1 t1) H0) in (eq_ind K k
298 (\lambda (k1: K).((eq T v0 v1) \to ((eq T t0 t1) \to ((eq T (THead k1 v2 t2)
299 u2) \to (ex_2 T T (\lambda (v3: T).(\lambda (t3: T).(eq T u2 (THead k v3
300 t3))))))))) (\lambda (H5: (eq T v0 v1)).(eq_ind T v1 (\lambda (_: T).((eq T
301 t0 t1) \to ((eq T (THead k v2 t2) u2) \to (ex_2 T T (\lambda (v3: T).(\lambda
302 (t3: T).(eq T u2 (THead k v3 t3)))))))) (\lambda (H6: (eq T t0 t1)).(eq_ind T
303 t1 (\lambda (_: T).((eq T (THead k v2 t2) u2) \to (ex_2 T T (\lambda (v3:
304 T).(\lambda (t3: T).(eq T u2 (THead k v3 t3))))))) (\lambda (H7: (eq T (THead
305 k v2 t2) u2)).(eq_ind T (THead k v2 t2) (\lambda (t: T).(ex_2 T T (\lambda
306 (v3: T).(\lambda (t3: T).(eq T t (THead k v3 t3)))))) (ex_2_intro T T
307 (\lambda (v3: T).(\lambda (t3: T).(eq T (THead k v2 t2) (THead k v3 t3)))) v2
308 t2 (refl_equal T (THead k v2 t2))) u2 H7)) t0 (sym_eq T t0 t1 H6))) v0
309 (sym_eq T v0 v1 H5))) k0 (sym_eq K k0 k H4))) H3)) H2)) H1)))]) in (H0
310 (refl_equal T (THead k v1 t1)) (refl_equal T u2))))))).