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 "LambdaDelta-1/csubv/defs.ma".
19 include "LambdaDelta-1/clear/fwd.ma".
21 theorem csubv_clear_conf:
22 \forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (b1:
23 B).(\forall (d1: C).(\forall (v1: T).((clear c1 (CHead d1 (Bind b1) v1)) \to
24 (ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1
25 d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(clear c2 (CHead d2
26 (Bind b2) v2))))))))))))
28 \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubv c1 c2)).(csubv_ind
29 (\lambda (c: C).(\lambda (c0: C).(\forall (b1: B).(\forall (d1: C).(\forall
30 (v1: T).((clear c (CHead d1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (_:
31 B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2:
32 B).(\lambda (d2: C).(\lambda (v2: T).(clear c0 (CHead d2 (Bind b2)
33 v2)))))))))))) (\lambda (n: nat).(\lambda (b1: B).(\lambda (d1: C).(\lambda
34 (v1: T).(\lambda (H0: (clear (CSort n) (CHead d1 (Bind b1)
35 v1))).(clear_gen_sort (CHead d1 (Bind b1) v1) n H0 (ex2_3 B C T (\lambda (_:
36 B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2:
37 B).(\lambda (d2: C).(\lambda (v2: T).(clear (CSort n) (CHead d2 (Bind b2)
38 v2)))))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (csubv c3
39 c4)).(\lambda (_: ((\forall (b1: B).(\forall (d1: C).(\forall (v1: T).((clear
40 c3 (CHead d1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (_: B).(\lambda (d2:
41 C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2:
42 C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind b2) v2)))))))))))).(\lambda
43 (v1: T).(\lambda (v2: T).(\lambda (b1: B).(\lambda (d1: C).(\lambda (v0:
44 T).(\lambda (H2: (clear (CHead c3 (Bind Void) v1) (CHead d1 (Bind b1)
45 v0))).(let H3 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
46 (_: C).C) with [(CSort _) \Rightarrow d1 | (CHead c _ _) \Rightarrow c]))
47 (CHead d1 (Bind b1) v0) (CHead c3 (Bind Void) v1) (clear_gen_bind Void c3
48 (CHead d1 (Bind b1) v0) v1 H2)) in ((let H4 \def (f_equal C B (\lambda (e:
49 C).(match e in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow b1 |
50 (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind
51 b) \Rightarrow b | (Flat _) \Rightarrow b1])])) (CHead d1 (Bind b1) v0)
52 (CHead c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind b1) v0) v1
53 H2)) in ((let H5 \def (f_equal C T (\lambda (e: C).(match e in C return
54 (\lambda (_: C).T) with [(CSort _) \Rightarrow v0 | (CHead _ _ t) \Rightarrow
55 t])) (CHead d1 (Bind b1) v0) (CHead c3 (Bind Void) v1) (clear_gen_bind Void
56 c3 (CHead d1 (Bind b1) v0) v1 H2)) in (\lambda (_: (eq B b1 Void)).(\lambda
57 (H7: (eq C d1 c3)).(eq_ind_r C c3 (\lambda (c: C).(ex2_3 B C T (\lambda (_:
58 B).(\lambda (d2: C).(\lambda (_: T).(csubv c d2)))) (\lambda (b2: B).(\lambda
59 (d2: C).(\lambda (v3: T).(clear (CHead c4 (Bind Void) v2) (CHead d2 (Bind b2)
60 v3))))))) (ex2_3_intro B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
61 T).(csubv c3 d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear
62 (CHead c4 (Bind Void) v2) (CHead d2 (Bind b2) v3))))) Void c4 v2 H0
63 (clear_bind Void c4 v2)) d1 H7)))) H4)) H3)))))))))))) (\lambda (c3:
64 C).(\lambda (c4: C).(\lambda (H0: (csubv c3 c4)).(\lambda (_: ((\forall (b1:
65 B).(\forall (d1: C).(\forall (v1: T).((clear c3 (CHead d1 (Bind b1) v1)) \to
66 (ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1
67 d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(clear c4 (CHead d2
68 (Bind b2) v2)))))))))))).(\lambda (b1: B).(\lambda (_: (not (eq B b1
69 Void))).(\lambda (b2: B).(\lambda (v1: T).(\lambda (v2: T).(\lambda (b0:
70 B).(\lambda (d1: C).(\lambda (v0: T).(\lambda (H3: (clear (CHead c3 (Bind b1)
71 v1) (CHead d1 (Bind b0) v0))).(let H4 \def (f_equal C C (\lambda (e:
72 C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d1 |
73 (CHead c _ _) \Rightarrow c])) (CHead d1 (Bind b0) v0) (CHead c3 (Bind b1)
74 v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3)) in ((let H5 \def
75 (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with
76 [(CSort _) \Rightarrow b0 | (CHead _ k _) \Rightarrow (match k in K return
77 (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow
78 b0])])) (CHead d1 (Bind b0) v0) (CHead c3 (Bind b1) v1) (clear_gen_bind b1 c3
79 (CHead d1 (Bind b0) v0) v1 H3)) in ((let H6 \def (f_equal C T (\lambda (e:
80 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow v0 |
81 (CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind b0) v0) (CHead c3 (Bind b1)
82 v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3)) in (\lambda (_: (eq
83 B b0 b1)).(\lambda (H8: (eq C d1 c3)).(eq_ind_r C c3 (\lambda (c: C).(ex2_3 B
84 C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv c d2)))) (\lambda
85 (b3: B).(\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Bind b2) v2)
86 (CHead d2 (Bind b3) v3))))))) (ex2_3_intro B C T (\lambda (_: B).(\lambda
87 (d2: C).(\lambda (_: T).(csubv c3 d2)))) (\lambda (b3: B).(\lambda (d2:
88 C).(\lambda (v3: T).(clear (CHead c4 (Bind b2) v2) (CHead d2 (Bind b3)
89 v3))))) b2 c4 v2 H0 (clear_bind b2 c4 v2)) d1 H8)))) H5)) H4)))))))))))))))
90 (\lambda (c3: C).(\lambda (c4: C).(\lambda (_: (csubv c3 c4)).(\lambda (H1:
91 ((\forall (b1: B).(\forall (d1: C).(\forall (v1: T).((clear c3 (CHead d1
92 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
93 T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(clear
94 c4 (CHead d2 (Bind b2) v2)))))))))))).(\lambda (f1: F).(\lambda (f2:
95 F).(\lambda (v1: T).(\lambda (v2: T).(\lambda (b1: B).(\lambda (d1:
96 C).(\lambda (v0: T).(\lambda (H2: (clear (CHead c3 (Flat f1) v1) (CHead d1
97 (Bind b1) v0))).(let H_x \def (H1 b1 d1 v0 (clear_gen_flat f1 c3 (CHead d1
98 (Bind b1) v0) v1 H2)) in (let H3 \def H_x in (ex2_3_ind B C T (\lambda (_:
99 B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2:
100 B).(\lambda (d2: C).(\lambda (v3: T).(clear c4 (CHead d2 (Bind b2) v3)))))
101 (ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1
102 d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4
103 (Flat f2) v2) (CHead d2 (Bind b2) v3)))))) (\lambda (x0: B).(\lambda (x1:
104 C).(\lambda (x2: T).(\lambda (H4: (csubv d1 x1)).(\lambda (H5: (clear c4
105 (CHead x1 (Bind x0) x2))).(ex2_3_intro B C T (\lambda (_: B).(\lambda (d2:
106 C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2:
107 C).(\lambda (v3: T).(clear (CHead c4 (Flat f2) v2) (CHead d2 (Bind b2)
108 v3))))) x0 x1 x2 H4 (clear_flat c4 (CHead x1 (Bind x0) x2) H5 f2 v2)))))))
109 H3))))))))))))))) c1 c2 H))).
111 theorem csubv_clear_conf_void:
112 \forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (d1:
113 C).(\forall (v1: T).((clear c1 (CHead d1 (Bind Void) v1)) \to (ex2_2 C T
114 (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2: C).(\lambda
115 (v2: T).(clear c2 (CHead d2 (Bind Void) v2))))))))))
117 \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubv c1 c2)).(csubv_ind
118 (\lambda (c: C).(\lambda (c0: C).(\forall (d1: C).(\forall (v1: T).((clear c
119 (CHead d1 (Bind Void) v1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (_:
120 T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(clear c0 (CHead d2
121 (Bind Void) v2)))))))))) (\lambda (n: nat).(\lambda (d1: C).(\lambda (v1:
122 T).(\lambda (H0: (clear (CSort n) (CHead d1 (Bind Void) v1))).(clear_gen_sort
123 (CHead d1 (Bind Void) v1) n H0 (ex2_2 C T (\lambda (d2: C).(\lambda (_:
124 T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(clear (CSort n) (CHead
125 d2 (Bind Void) v2)))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0:
126 (csubv c3 c4)).(\lambda (_: ((\forall (d1: C).(\forall (v1: T).((clear c3
127 (CHead d1 (Bind Void) v1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (_:
128 T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(clear c4 (CHead d2
129 (Bind Void) v2)))))))))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (d1:
130 C).(\lambda (v0: T).(\lambda (H2: (clear (CHead c3 (Bind Void) v1) (CHead d1
131 (Bind Void) v0))).(let H3 \def (f_equal C C (\lambda (e: C).(match e in C
132 return (\lambda (_: C).C) with [(CSort _) \Rightarrow d1 | (CHead c _ _)
133 \Rightarrow c])) (CHead d1 (Bind Void) v0) (CHead c3 (Bind Void) v1)
134 (clear_gen_bind Void c3 (CHead d1 (Bind Void) v0) v1 H2)) in ((let H4 \def
135 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
136 [(CSort _) \Rightarrow v0 | (CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind
137 Void) v0) (CHead c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind
138 Void) v0) v1 H2)) in (\lambda (H5: (eq C d1 c3)).(eq_ind_r C c3 (\lambda (c:
139 C).(ex2_2 C T (\lambda (d2: C).(\lambda (_: T).(csubv c d2))) (\lambda (d2:
140 C).(\lambda (v3: T).(clear (CHead c4 (Bind Void) v2) (CHead d2 (Bind Void)
141 v3)))))) (ex2_2_intro C T (\lambda (d2: C).(\lambda (_: T).(csubv c3 d2)))
142 (\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Bind Void) v2) (CHead d2
143 (Bind Void) v3)))) c4 v2 H0 (clear_bind Void c4 v2)) d1 H5))) H3)))))))))))
144 (\lambda (c3: C).(\lambda (c4: C).(\lambda (_: (csubv c3 c4)).(\lambda (_:
145 ((\forall (d1: C).(\forall (v1: T).((clear c3 (CHead d1 (Bind Void) v1)) \to
146 (ex2_2 C T (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2:
147 C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind Void) v2)))))))))).(\lambda
148 (b1: B).(\lambda (H2: (not (eq B b1 Void))).(\lambda (b2: B).(\lambda (v1:
149 T).(\lambda (v2: T).(\lambda (d1: C).(\lambda (v0: T).(\lambda (H3: (clear
150 (CHead c3 (Bind b1) v1) (CHead d1 (Bind Void) v0))).(let H4 \def (f_equal C C
151 (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
152 \Rightarrow d1 | (CHead c _ _) \Rightarrow c])) (CHead d1 (Bind Void) v0)
153 (CHead c3 (Bind b1) v1) (clear_gen_bind b1 c3 (CHead d1 (Bind Void) v0) v1
154 H3)) in ((let H5 \def (f_equal C B (\lambda (e: C).(match e in C return
155 (\lambda (_: C).B) with [(CSort _) \Rightarrow Void | (CHead _ k _)
156 \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
157 \Rightarrow b | (Flat _) \Rightarrow Void])])) (CHead d1 (Bind Void) v0)
158 (CHead c3 (Bind b1) v1) (clear_gen_bind b1 c3 (CHead d1 (Bind Void) v0) v1
159 H3)) in ((let H6 \def (f_equal C T (\lambda (e: C).(match e in C return
160 (\lambda (_: C).T) with [(CSort _) \Rightarrow v0 | (CHead _ _ t) \Rightarrow
161 t])) (CHead d1 (Bind Void) v0) (CHead c3 (Bind b1) v1) (clear_gen_bind b1 c3
162 (CHead d1 (Bind Void) v0) v1 H3)) in (\lambda (H7: (eq B Void b1)).(\lambda
163 (H8: (eq C d1 c3)).(eq_ind_r C c3 (\lambda (c: C).(ex2_2 C T (\lambda (d2:
164 C).(\lambda (_: T).(csubv c d2))) (\lambda (d2: C).(\lambda (v3: T).(clear
165 (CHead c4 (Bind b2) v2) (CHead d2 (Bind Void) v3)))))) (let H9 \def (eq_ind_r
166 B b1 (\lambda (b: B).(not (eq B b Void))) H2 Void H7) in (let H10 \def (match
167 (H9 (refl_equal B Void)) in False return (\lambda (_: False).(ex2_2 C T
168 (\lambda (d2: C).(\lambda (_: T).(csubv c3 d2))) (\lambda (d2: C).(\lambda
169 (v3: T).(clear (CHead c4 (Bind b2) v2) (CHead d2 (Bind Void) v3)))))) with
170 []) in H10)) d1 H8)))) H5)) H4)))))))))))))) (\lambda (c3: C).(\lambda (c4:
171 C).(\lambda (_: (csubv c3 c4)).(\lambda (H1: ((\forall (d1: C).(\forall (v1:
172 T).((clear c3 (CHead d1 (Bind Void) v1)) \to (ex2_2 C T (\lambda (d2:
173 C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(clear
174 c4 (CHead d2 (Bind Void) v2)))))))))).(\lambda (f1: F).(\lambda (f2:
175 F).(\lambda (v1: T).(\lambda (v2: T).(\lambda (d1: C).(\lambda (v0:
176 T).(\lambda (H2: (clear (CHead c3 (Flat f1) v1) (CHead d1 (Bind Void)
177 v0))).(let H_x \def (H1 d1 v0 (clear_gen_flat f1 c3 (CHead d1 (Bind Void) v0)
178 v1 H2)) in (let H3 \def H_x in (ex2_2_ind C T (\lambda (d2: C).(\lambda (_:
179 T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v3: T).(clear c4 (CHead d2
180 (Bind Void) v3)))) (ex2_2 C T (\lambda (d2: C).(\lambda (_: T).(csubv d1
181 d2))) (\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Flat f2) v2) (CHead
182 d2 (Bind Void) v3))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H4: (csubv
183 d1 x0)).(\lambda (H5: (clear c4 (CHead x0 (Bind Void) x1))).(ex2_2_intro C T
184 (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2: C).(\lambda
185 (v3: T).(clear (CHead c4 (Flat f2) v2) (CHead d2 (Bind Void) v3)))) x0 x1 H4
186 (clear_flat c4 (CHead x0 (Bind Void) x1) H5 f2 v2)))))) H3)))))))))))))) c1