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 "basic_1A/nf2/defs.ma".
19 include "basic_1A/pr2/clen.ma".
21 include "basic_1A/pr0/dec.ma".
23 include "basic_1A/C/props.ma".
26 \forall (c: C).(\forall (t1: T).(or (nf2 c t1) (ex2 T (\lambda (t2: T).((eq
27 T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 c t1 t2)))))
29 \lambda (c: C).(c_tail_ind (\lambda (c0: C).(\forall (t1: T).(or (\forall
30 (t2: T).((pr2 c0 t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1
31 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 c0 t1 t2)))))) (\lambda
32 (n: nat).(\lambda (t1: T).(let H_x \def (nf0_dec t1) in (let H \def H_x in
33 (or_ind (\forall (t2: T).((pr0 t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2:
34 T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t1 t2)))
35 (or (\forall (t2: T).((pr2 (CSort n) t1 t2) \to (eq T t1 t2))) (ex2 T
36 (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2:
37 T).(pr2 (CSort n) t1 t2)))) (\lambda (H0: ((\forall (t2: T).((pr0 t1 t2) \to
38 (eq T t1 t2))))).(or_introl (\forall (t2: T).((pr2 (CSort n) t1 t2) \to (eq T
39 t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
40 (\lambda (t2: T).(pr2 (CSort n) t1 t2))) (\lambda (t2: T).(\lambda (H1: (pr2
41 (CSort n) t1 t2)).(let H_y \def (pr2_gen_csort t1 t2 n H1) in (H0 t2
42 H_y)))))) (\lambda (H0: (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall
43 (P: Prop).P))) (\lambda (t2: T).(pr0 t1 t2)))).(ex2_ind T (\lambda (t2:
44 T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t1 t2))
45 (or (\forall (t2: T).((pr2 (CSort n) t1 t2) \to (eq T t1 t2))) (ex2 T
46 (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2:
47 T).(pr2 (CSort n) t1 t2)))) (\lambda (x: T).(\lambda (H1: (((eq T t1 x) \to
48 (\forall (P: Prop).P)))).(\lambda (H2: (pr0 t1 x)).(or_intror (\forall (t2:
49 T).((pr2 (CSort n) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T
50 t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CSort n) t1 t2)))
51 (ex_intro2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
52 (\lambda (t2: T).(pr2 (CSort n) t1 t2)) x H1 (pr2_free (CSort n) t1 x
53 H2)))))) H0)) H))))) (\lambda (c0: C).(\lambda (H: ((\forall (t1: T).(or
54 (\forall (t2: T).((pr2 c0 t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2:
55 T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 c0 t1
56 t2))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (t1: T).(let H_x \def (H
57 t1) in (let H0 \def H_x in (or_ind (\forall (t2: T).((pr2 c0 t1 t2) \to (eq T
58 t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
59 (\lambda (t2: T).(pr2 c0 t1 t2))) (or (\forall (t2: T).((pr2 (CTail k t c0)
60 t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall
61 (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail k t c0) t1 t2)))) (\lambda (H1:
62 ((\forall (t2: T).((pr2 c0 t1 t2) \to (eq T t1 t2))))).(K_ind (\lambda (k0:
63 K).(or (\forall (t2: T).((pr2 (CTail k0 t c0) t1 t2) \to (eq T t1 t2))) (ex2
64 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2:
65 T).(pr2 (CTail k0 t c0) t1 t2))))) (\lambda (b: B).(B_ind (\lambda (b0:
66 B).(or (\forall (t2: T).((pr2 (CTail (Bind b0) t c0) t1 t2) \to (eq T t1
67 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
68 (\lambda (t2: T).(pr2 (CTail (Bind b0) t c0) t1 t2))))) (let H_x0 \def
69 (dnf_dec t t1 (clen c0)) in (let H2 \def H_x0 in (ex_ind T (\lambda (v:
70 T).(or (subst0 (clen c0) t t1 (lift (S O) (clen c0) v)) (eq T t1 (lift (S O)
71 (clen c0) v)))) (or (\forall (t2: T).((pr2 (CTail (Bind Abbr) t c0) t1 t2)
72 \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P:
73 Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) t1 t2)))) (\lambda
74 (x: T).(\lambda (H3: (or (subst0 (clen c0) t t1 (lift (S O) (clen c0) x)) (eq
75 T t1 (lift (S O) (clen c0) x)))).(or_ind (subst0 (clen c0) t t1 (lift (S O)
76 (clen c0) x)) (eq T t1 (lift (S O) (clen c0) x)) (or (\forall (t2: T).((pr2
77 (CTail (Bind Abbr) t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2:
78 T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail
79 (Bind Abbr) t c0) t1 t2)))) (\lambda (H4: (subst0 (clen c0) t t1 (lift (S O)
80 (clen c0) x))).(let H_x1 \def (getl_ctail_clen Abbr t c0) in (let H5 \def
81 H_x1 in (ex_ind nat (\lambda (n: nat).(getl (clen c0) (CTail (Bind Abbr) t
82 c0) (CHead (CSort n) (Bind Abbr) t))) (or (\forall (t2: T).((pr2 (CTail (Bind
83 Abbr) t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2)
84 \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) t1
85 t2)))) (\lambda (x0: nat).(\lambda (H6: (getl (clen c0) (CTail (Bind Abbr) t
86 c0) (CHead (CSort x0) (Bind Abbr) t))).(or_intror (\forall (t2: T).((pr2
87 (CTail (Bind Abbr) t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2:
88 T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail
89 (Bind Abbr) t c0) t1 t2))) (ex_intro2 T (\lambda (t2: T).((eq T t1 t2) \to
90 (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) t1
91 t2)) (lift (S O) (clen c0) x) (\lambda (H7: (eq T t1 (lift (S O) (clen c0)
92 x))).(\lambda (P: Prop).(let H8 \def (eq_ind T t1 (\lambda (t0: T).(subst0
93 (clen c0) t t0 (lift (S O) (clen c0) x))) H4 (lift (S O) (clen c0) x) H7) in
94 (subst0_gen_lift_false x t (lift (S O) (clen c0) x) (S O) (clen c0) (clen c0)
95 (le_n (clen c0)) (eq_ind_r nat (plus (S O) (clen c0)) (\lambda (n: nat).(lt
96 (clen c0) n)) (le_n (plus (S O) (clen c0))) (plus (clen c0) (S O)) (plus_sym
97 (clen c0) (S O))) H8 P)))) (pr2_delta (CTail (Bind Abbr) t c0) (CSort x0) t
98 (clen c0) H6 t1 t1 (pr0_refl t1) (lift (S O) (clen c0) x) H4))))) H5))))
99 (\lambda (H4: (eq T t1 (lift (S O) (clen c0) x))).(let H5 \def (eq_ind T t1
100 (\lambda (t0: T).(\forall (t2: T).((pr2 c0 t0 t2) \to (eq T t0 t2)))) H1
101 (lift (S O) (clen c0) x) H4) in (eq_ind_r T (lift (S O) (clen c0) x) (\lambda
102 (t0: T).(or (\forall (t2: T).((pr2 (CTail (Bind Abbr) t c0) t0 t2) \to (eq T
103 t0 t2))) (ex2 T (\lambda (t2: T).((eq T t0 t2) \to (\forall (P: Prop).P)))
104 (\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) t0 t2))))) (or_introl (\forall
105 (t2: T).((pr2 (CTail (Bind Abbr) t c0) (lift (S O) (clen c0) x) t2) \to (eq T
106 (lift (S O) (clen c0) x) t2))) (ex2 T (\lambda (t2: T).((eq T (lift (S O)
107 (clen c0) x) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail
108 (Bind Abbr) t c0) (lift (S O) (clen c0) x) t2))) (\lambda (t2: T).(\lambda
109 (H6: (pr2 (CTail (Bind Abbr) t c0) (lift (S O) (clen c0) x) t2)).(let H_x1
110 \def (pr2_gen_ctail (Bind Abbr) c0 t (lift (S O) (clen c0) x) t2 H6) in (let
111 H7 \def H_x1 in (or_ind (pr2 c0 (lift (S O) (clen c0) x) t2) (ex3 T (\lambda
112 (_: T).(eq K (Bind Abbr) (Bind Abbr))) (\lambda (t0: T).(pr0 (lift (S O)
113 (clen c0) x) t0)) (\lambda (t0: T).(subst0 (clen c0) t t0 t2))) (eq T (lift
114 (S O) (clen c0) x) t2) (\lambda (H8: (pr2 c0 (lift (S O) (clen c0) x)
115 t2)).(H5 t2 H8)) (\lambda (H8: (ex3 T (\lambda (_: T).(eq K (Bind Abbr) (Bind
116 Abbr))) (\lambda (t0: T).(pr0 (lift (S O) (clen c0) x) t0)) (\lambda (t0:
117 T).(subst0 (clen c0) t t0 t2)))).(ex3_ind T (\lambda (_: T).(eq K (Bind Abbr)
118 (Bind Abbr))) (\lambda (t0: T).(pr0 (lift (S O) (clen c0) x) t0)) (\lambda
119 (t0: T).(subst0 (clen c0) t t0 t2)) (eq T (lift (S O) (clen c0) x) t2)
120 (\lambda (x0: T).(\lambda (_: (eq K (Bind Abbr) (Bind Abbr))).(\lambda (H10:
121 (pr0 (lift (S O) (clen c0) x) x0)).(\lambda (H11: (subst0 (clen c0) t x0
122 t2)).(ex2_ind T (\lambda (t3: T).(eq T x0 (lift (S O) (clen c0) t3)))
123 (\lambda (t3: T).(pr0 x t3)) (eq T (lift (S O) (clen c0) x) t2) (\lambda (x1:
124 T).(\lambda (H12: (eq T x0 (lift (S O) (clen c0) x1))).(\lambda (_: (pr0 x
125 x1)).(let H14 \def (eq_ind T x0 (\lambda (t0: T).(subst0 (clen c0) t t0 t2))
126 H11 (lift (S O) (clen c0) x1) H12) in (subst0_gen_lift_false x1 t t2 (S O)
127 (clen c0) (clen c0) (le_n (clen c0)) (eq_ind_r nat (plus (S O) (clen c0))
128 (\lambda (n: nat).(lt (clen c0) n)) (le_n (plus (S O) (clen c0))) (plus (clen
129 c0) (S O)) (plus_sym (clen c0) (S O))) H14 (eq T (lift (S O) (clen c0) x)
130 t2)))))) (pr0_gen_lift x x0 (S O) (clen c0) H10)))))) H8)) H7)))))) t1 H4)))
131 H3))) H2))) (or_introl (\forall (t2: T).((pr2 (CTail (Bind Abst) t c0) t1 t2)
132 \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P:
133 Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind Abst) t c0) t1 t2))) (\lambda
134 (t2: T).(\lambda (H2: (pr2 (CTail (Bind Abst) t c0) t1 t2)).(let H_x0 \def
135 (pr2_gen_ctail (Bind Abst) c0 t t1 t2 H2) in (let H3 \def H_x0 in (or_ind
136 (pr2 c0 t1 t2) (ex3 T (\lambda (_: T).(eq K (Bind Abst) (Bind Abbr)))
137 (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0: T).(subst0 (clen c0) t t0 t2)))
138 (eq T t1 t2) (\lambda (H4: (pr2 c0 t1 t2)).(H1 t2 H4)) (\lambda (H4: (ex3 T
139 (\lambda (_: T).(eq K (Bind Abst) (Bind Abbr))) (\lambda (t0: T).(pr0 t1 t0))
140 (\lambda (t0: T).(subst0 (clen c0) t t0 t2)))).(ex3_ind T (\lambda (_: T).(eq
141 K (Bind Abst) (Bind Abbr))) (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0:
142 T).(subst0 (clen c0) t t0 t2)) (eq T t1 t2) (\lambda (x0: T).(\lambda (H5:
143 (eq K (Bind Abst) (Bind Abbr))).(\lambda (_: (pr0 t1 x0)).(\lambda (_:
144 (subst0 (clen c0) t x0 t2)).(let H8 \def (eq_ind K (Bind Abst) (\lambda (ee:
145 K).(match ee with [(Bind b0) \Rightarrow (match b0 with [Abbr \Rightarrow
146 False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _)
147 \Rightarrow False])) I (Bind Abbr) H5) in (False_ind (eq T t1 t2) H8))))))
148 H4)) H3)))))) (or_introl (\forall (t2: T).((pr2 (CTail (Bind Void) t c0) t1
149 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P:
150 Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind Void) t c0) t1 t2))) (\lambda
151 (t2: T).(\lambda (H2: (pr2 (CTail (Bind Void) t c0) t1 t2)).(let H_x0 \def
152 (pr2_gen_ctail (Bind Void) c0 t t1 t2 H2) in (let H3 \def H_x0 in (or_ind
153 (pr2 c0 t1 t2) (ex3 T (\lambda (_: T).(eq K (Bind Void) (Bind Abbr)))
154 (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0: T).(subst0 (clen c0) t t0 t2)))
155 (eq T t1 t2) (\lambda (H4: (pr2 c0 t1 t2)).(H1 t2 H4)) (\lambda (H4: (ex3 T
156 (\lambda (_: T).(eq K (Bind Void) (Bind Abbr))) (\lambda (t0: T).(pr0 t1 t0))
157 (\lambda (t0: T).(subst0 (clen c0) t t0 t2)))).(ex3_ind T (\lambda (_: T).(eq
158 K (Bind Void) (Bind Abbr))) (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0:
159 T).(subst0 (clen c0) t t0 t2)) (eq T t1 t2) (\lambda (x0: T).(\lambda (H5:
160 (eq K (Bind Void) (Bind Abbr))).(\lambda (_: (pr0 t1 x0)).(\lambda (_:
161 (subst0 (clen c0) t x0 t2)).(let H8 \def (eq_ind K (Bind Void) (\lambda (ee:
162 K).(match ee with [(Bind b0) \Rightarrow (match b0 with [Abbr \Rightarrow
163 False | Abst \Rightarrow False | Void \Rightarrow True]) | (Flat _)
164 \Rightarrow False])) I (Bind Abbr) H5) in (False_ind (eq T t1 t2) H8))))))
165 H4)) H3)))))) b)) (\lambda (f: F).(or_introl (\forall (t2: T).((pr2 (CTail
166 (Flat f) t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1
167 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Flat f) t c0)
168 t1 t2))) (\lambda (t2: T).(\lambda (H2: (pr2 (CTail (Flat f) t c0) t1
169 t2)).(let H_x0 \def (pr2_gen_ctail (Flat f) c0 t t1 t2 H2) in (let H3 \def
170 H_x0 in (or_ind (pr2 c0 t1 t2) (ex3 T (\lambda (_: T).(eq K (Flat f) (Bind
171 Abbr))) (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0: T).(subst0 (clen c0) t t0
172 t2))) (eq T t1 t2) (\lambda (H4: (pr2 c0 t1 t2)).(H1 t2 H4)) (\lambda (H4:
173 (ex3 T (\lambda (_: T).(eq K (Flat f) (Bind Abbr))) (\lambda (t0: T).(pr0 t1
174 t0)) (\lambda (t0: T).(subst0 (clen c0) t t0 t2)))).(ex3_ind T (\lambda (_:
175 T).(eq K (Flat f) (Bind Abbr))) (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0:
176 T).(subst0 (clen c0) t t0 t2)) (eq T t1 t2) (\lambda (x0: T).(\lambda (H5:
177 (eq K (Flat f) (Bind Abbr))).(\lambda (_: (pr0 t1 x0)).(\lambda (_: (subst0
178 (clen c0) t x0 t2)).(let H8 \def (eq_ind K (Flat f) (\lambda (ee: K).(match
179 ee with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])) I (Bind
180 Abbr) H5) in (False_ind (eq T t1 t2) H8)))))) H4)) H3))))))) k)) (\lambda
181 (H1: (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
182 (\lambda (t2: T).(pr2 c0 t1 t2)))).(ex2_ind T (\lambda (t2: T).((eq T t1 t2)
183 \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 c0 t1 t2)) (or (\forall
184 (t2: T).((pr2 (CTail k t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2:
185 T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail k t
186 c0) t1 t2)))) (\lambda (x: T).(\lambda (H2: (((eq T t1 x) \to (\forall (P:
187 Prop).P)))).(\lambda (H3: (pr2 c0 t1 x)).(or_intror (\forall (t2: T).((pr2
188 (CTail k t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1
189 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail k t c0) t1 t2)))
190 (ex_intro2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
191 (\lambda (t2: T).(pr2 (CTail k t c0) t1 t2)) x H2 (pr2_ctail c0 t1 x H3 k
192 t)))))) H1)) H0)))))))) c).