]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/didactic/support/natural_deduction.ma
c592b5254a3df4469f5af82c49e1fb9b0f6c6276
[helm.git] / helm / software / matita / library / didactic / support / natural_deduction.ma
1 (* Logic system *)
2
3 inductive Imply (A,B:CProp) : CProp ≝
4 | Imply_intro: (A → B) → Imply A B.
5  
6 definition Imply_elim ≝ λA,B.λf:Imply A B. λa:A.
7   match f with [ Imply_intro g ⇒ g a].
8
9 inductive And (A,B:CProp) : CProp ≝
10 | And_intro: A → B → And A B.
11
12 definition And_elim_l ≝ λA,B.λc:And A B.
13   match c with [ And_intro a b ⇒ a ].
14
15 definition And_elim_r ≝ λA,B.λc:And A B.
16   match c with [ And_intro a b ⇒ b ].
17
18 inductive Or (A,B:CProp) : CProp ≝
19 | Or_intro_l: A → Or A B
20 | Or_intro_r: B → Or A B. 
21  
22 definition Or_elim ≝ λA,B,C:CProp.λc:Or A B.λfa: A → C.λfb: B → C.
23   match c with 
24   [ Or_intro_l a ⇒ fa a 
25   | Or_intro_r b ⇒ fb b].
26
27 inductive Top : CProp := 
28 | Top_intro : Top.
29
30 inductive Bot : CProp := .
31
32 definition Bot_elim ≝ λP:CProp.λx:Bot.
33   match x in Bot return λx.P with []. 
34
35 definition Not := λA:CProp.Imply A Bot.
36
37 definition Not_intro : ∀A.(A → Bot) → Not A ≝  λA. 
38   Imply_intro A Bot.
39
40 definition Not_elim : ∀A.Not A → A → Bot ≝ λA. 
41   Imply_elim ? Bot.  
42
43 definition Discharge := λA:CProp.λa:A.
44   a.
45
46 axiom Raa : ∀A.(Not A → Bot) → A.
47
48 axiom sort : Type.
49
50 inductive Exists (A:Type) (P:A→CProp) : CProp ≝
51   Exists_intro: ∀w:A. P w → Exists A P.
52
53 definition Exists_elim ≝
54   λA:Type.λP:A→CProp.λC:CProp.λc:Exists A P.λH:(Πx.P x → C).
55    match c with [ Exists_intro w p ⇒ H w p ].
56
57 inductive Forall (A:Type) (P:A→CProp) : CProp ≝
58  Forall_intro: (∀n:A. P n) → Forall A P.
59
60 definition Forall_elim ≝
61  λA:Type.λP:A→CProp.λn:A.λf:Forall A P.match f with [ Forall_intro g ⇒ g n ].
62
63 (* Dummy proposition *)
64 axiom unit : CProp.
65
66 (* Notations *)
67 notation "hbox(a break ⇒ b)" right associative with precedence 20 
68 for @{ 'Imply $a $b }.
69 interpretation "Imply" 'Imply a b = (Imply a b).
70 interpretation "constructive or" 'or x y = (Or x y).
71 interpretation "constructive and" 'and x y = (And x y).
72 notation "⊤" non associative with precedence 90 for @{'Top}.
73 interpretation "Top" 'Top = Top.
74 notation "⊥" non associative with precedence 90 for @{'Bot}.
75 interpretation "Bot" 'Bot = Bot.
76 interpretation "Not" 'not a = (Not a).
77 notation "✶" non associative with precedence 90 for @{'unit}.
78 interpretation "dummy prop" 'unit = unit.
79 notation > "\exists list1 ident x sep , . term 19 Px" with precedence 20
80 for ${ fold right @{$Px} rec acc @{'myexists (λ${ident x}.$acc)} }.
81 notation < "hvbox(\exists ident i break . p)" with precedence 20
82 for @{ 'myexists (\lambda ${ident i} : $ty. $p) }.
83 interpretation "constructive ex" 'myexists \eta.x = (Exists sort x).
84 notation > "\forall ident x.break term 19 Px" with precedence 20
85 for @{ 'Forall (λ${ident x}.$Px) }.
86 notation < "\forall ident x.break term 19 Px" with precedence 20
87 for @{ 'Forall (λ${ident x}:$tx.$Px) }.
88 interpretation "Forall" 'Forall \eta.Px = (Forall _ Px).
89  
90 (* Variables *)
91 axiom A : CProp.
92 axiom B : CProp.
93 axiom C : CProp.
94 axiom D : CProp.
95 axiom E : CProp.
96 axiom F : CProp.
97 axiom G : CProp.
98 axiom H : CProp.
99 axiom I : CProp.
100 axiom J : CProp.
101 axiom K : CProp.
102 axiom L : CProp.
103 axiom M : CProp.
104 axiom N : CProp.
105 axiom O : CProp.
106 axiom  x: sort.
107 axiom  y: sort.
108 axiom  z: sort.
109 axiom  w: sort.
110
111 (* Every formula user provided annotates its proof:
112    `A` becomes `(show A ?)` *)
113 definition show : ΠA.A→A ≝ λA:CProp.λa:A.a.
114
115 (* When something does not fit, this daemon is used *)
116 axiom cast: ΠA,B:CProp.B → A.
117
118 (* begin a proof: draws the root *)
119 notation > "'prove' p" non associative with precedence 19 
120 for @{ 'prove $p }.
121 interpretation "prove KO" 'prove p = (cast _ _ (show p _)).
122 interpretation "prove OK" 'prove p = (show p _).
123
124 (* Leaves *)
125 notation < "\infrule (t\atop ⋮) a ?" with precedence 19
126 for @{ 'leaf_ok $a $t }.
127 interpretation "leaf OK" 'leaf_ok a t = (show a t).
128 notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19 
129 for @{ 'leaf_ko $a $t }.
130 interpretation "leaf KO" 'leaf_ko a t = (cast _ _ (show a t)).
131
132 (* discharging *)
133 notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 
134 for @{ 'discharge_ko_1 $a $H }.
135 interpretation "discharge_ko_1" 'discharge_ko_1 a H = 
136   (show a (cast _ _ (Discharge _ H))).
137 notation < "[ mstyle color #ff0000 (a) ] \sup mstyle color #ff0000 (H)" with precedence 19 
138 for @{ 'discharge_ko_2 $a $H }.
139 interpretation "discharge_ko_2" 'discharge_ko_2 a H = 
140   (cast _ _ (show a (cast _ _ (Discharge _ H)))).
141
142 notation < "[ a ] \sup H" with precedence 19 
143 for @{ 'discharge_ok_1 $a $H }.
144 interpretation "discharge_ok_1" 'discharge_ok_1 a H = 
145   (show a (Discharge _ H)).
146 notation < "[ mstyle color #ff0000 (a) ] \sup H" with precedence 19 
147 for @{ 'discharge_ok_2 $a $H }.
148 interpretation "discharge_ok_2" 'discharge_ok_2 a H = 
149   (cast _ _ (show a (Discharge _ H))).
150
151 notation > "'discharge' [H]" with precedence 19 
152 for @{ 'discharge $H }.
153 interpretation "discharge KO" 'discharge H = (cast _ _ (Discharge _ H)).
154 interpretation "discharge OK" 'discharge H = (Discharge _ H).
155
156 (* ⇒ introduction *)
157 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
158 for @{ 'Imply_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
159 interpretation "Imply_intro_ko_1" 'Imply_intro_ko_1 ab \eta.b = 
160   (show ab (cast _ _ (Imply_intro _ _ b))).
161
162 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
163 for @{ 'Imply_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
164 interpretation "Imply_intro_ko_2" 'Imply_intro_ko_2 ab \eta.b = 
165   (cast _ _ (show ab (cast _ _ (Imply_intro _ _ b)))).
166
167 notation < "maction (\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) ) (\vdots)" with precedence 19
168 for @{ 'Imply_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
169 interpretation "Imply_intro_ok_1" 'Imply_intro_ok_1 ab \eta.b = 
170   (show ab (Imply_intro _ _ b)).
171
172 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (⇒\sub\i \emsp ident H) " with precedence 19
173 for @{ 'Imply_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
174 interpretation "Imply_intro_ok_2" 'Imply_intro_ok_2 ab \eta.b = 
175   (cast _ _ (show ab (Imply_intro _ _ b))).
176
177 notation > "⇒_'i' [ident H] term 90 b" with precedence 19
178 for @{ 'Imply_intro $b (λ${ident H}.show $b ?) }.
179 interpretation "Imply_intro KO" 'Imply_intro b pb = 
180   (cast _ (Imply unit b) (Imply_intro _ b pb)).
181 interpretation "Imply_intro OK" 'Imply_intro b pb = 
182   (Imply_intro _ b pb).
183
184 (* ⇒ elimination *)
185 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19
186 for @{ 'Imply_elim_ko_1 $ab $a $b }.
187 interpretation "Imply_elim_ko_1" 'Imply_elim_ko_1 ab a b = 
188   (show b (cast _ _ (Imply_elim _ _ (cast _ _ ab) (cast _ _ a)))).
189
190 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19 
191 for @{ 'Imply_elim_ko_2 $ab $a $b }.
192 interpretation "Imply_elim_ko_2" 'Imply_elim_ko_2 ab a b = 
193   (cast _ _ (show b (cast _ _ (Imply_elim _ _ (cast _ _ ab) (cast _ _ a))))).
194
195 notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) ) (\vdots)" with precedence 19 
196 for @{ 'Imply_elim_ok_1 $ab $a $b }.
197 interpretation "Imply_elim_ok_1" 'Imply_elim_ok_1 ab a b = 
198   (show b (Imply_elim _ _ ab a)).
199
200 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (⇒\sub\e) " with precedence 19 
201 for @{ 'Imply_elim_ok_2 $ab $a $b }.
202 interpretation "Imply_elim_ok_2" 'Imply_elim_ok_2 ab a b = 
203   (cast _ _ (show b (Imply_elim _ _ ab a))).
204
205 notation > "⇒_'e' term 90 ab term 90 a" with precedence 19 
206 for @{ 'Imply_elim (show $ab ?) (show $a ?) }.
207 interpretation "Imply_elim KO" 'Imply_elim ab a = 
208   (cast _ _ (Imply_elim _ _ (cast (Imply unit unit) _ ab) (cast unit _ a))).
209 interpretation "Imply_elim OK" 'Imply_elim ab a = 
210   (Imply_elim _ _ ab a). 
211
212 (* ∧ introduction *)
213 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19 
214 for @{ 'And_intro_ko_1 $a $b $ab }.
215 interpretation "And_intro_ko_1" 'And_intro_ko_1 a b ab = 
216   (show ab (cast _ _ (And_intro _ _ a b))).
217
218 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19 
219 for @{ 'And_intro_ko_2 $a $b $ab }.
220 interpretation "And_intro_ko_2" 'And_intro_ko_2 a b ab = 
221   (cast _ _ (show ab (cast _ _ (And_intro _ _ a b)))).
222
223 notation < "maction (\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)) (\vdots)" with precedence 19 
224 for @{ 'And_intro_ok_1 $a $b $ab }.
225 interpretation "And_intro_ok_1" 'And_intro_ok_1 a b ab = 
226   (show ab (And_intro _ _ a b)).
227
228 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) (∧\sub\i)" with precedence 19 
229 for @{ 'And_intro_ok_2 $a $b $ab }.
230 interpretation "And_intro_ok_2" 'And_intro_ok_2 a b ab = 
231   (cast _ _ (show ab (And_intro _ _ a b))).
232
233 notation > "∧_'i' term 90 a term 90 b" with precedence 19 
234 for @{ 'And_intro (show $a ?) (show $b ?) }.
235 interpretation "And_intro KO" 'And_intro a b = (cast _ _ (And_intro _ _ a b)).
236 interpretation "And_intro OK" 'And_intro a b = (And_intro _ _ a b).
237
238 (* ∧ elimination *)
239 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19 
240 for @{ 'And_elim_l_ko_1 $ab $a }.
241 interpretation "And_elim_l_ko_1" 'And_elim_l_ko_1 ab a = 
242   (show a (cast _ _ (And_elim_l _ _ (cast _ _ ab)))).
243
244 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19 
245 for @{ 'And_elim_l_ko_2 $ab $a }.
246 interpretation "And_elim_l_ko_2" 'And_elim_l_ko_2 ab a = 
247   (cast _ _ (show a (cast _ _ (And_elim_l _ _ (cast _ _ ab))))).
248
249 notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))) (\vdots)" with precedence 19 
250 for @{ 'And_elim_l_ok_1 $ab $a }.
251 interpretation "And_elim_l_ok_1" 'And_elim_l_ok_1 ab a = 
252   (show a (And_elim_l _ _ ab)).
253
254 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\l))" with precedence 19 
255 for @{ 'And_elim_l_ok_2 $ab $a }.
256 interpretation "And_elim_l_ok_2" 'And_elim_l_ok_2 ab a = 
257   (cast _ _ (show a (And_elim_l _ _ ab))).
258
259 notation > "∧_'e_l' term 90 ab" with precedence 19
260 for @{ 'And_elim_l (show $ab ?) }.
261 interpretation "And_elim_l KO" 'And_elim_l a = (cast _ _ (And_elim_l _ _ (cast (And unit unit) _ a))).
262 interpretation "And_elim_l OK" 'And_elim_l a = (And_elim_l _ _ a).
263
264 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19 
265 for @{ 'And_elim_r_ko_1 $ab $a }.
266 interpretation "And_elim_r_ko_1" 'And_elim_r_ko_1 ab a = 
267   (show a (cast _ _ (And_elim_r _ _ (cast _ _ ab)))).
268
269 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19 
270 for @{ 'And_elim_r_ko_2 $ab $a }.
271 interpretation "And_elim_r_ko_2" 'And_elim_r_ko_2 ab a = 
272   (cast _ _ (show a (cast _ _ (And_elim_r _ _ (cast _ _ ab))))).
273
274 notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))) (\vdots)" with precedence 19 
275 for @{ 'And_elim_r_ok_1 $ab $a }.
276 interpretation "And_elim_r_ok_1" 'And_elim_r_ok_1 ab a = 
277   (show a (And_elim_r _ _ ab)).
278
279 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\r))" with precedence 19 
280 for @{ 'And_elim_r_ok_2 $ab $a }.
281 interpretation "And_elim_r_ok_2" 'And_elim_r_ok_2 ab a = 
282   (cast _ _ (show a (And_elim_r _ _ ab))).
283
284 notation > "∧_'e_r' term 90 ab" with precedence 19
285 for @{ 'And_elim_r (show $ab ?) }.
286 interpretation "And_elim_r KO" 'And_elim_r a = (cast _ _ (And_elim_r _ _ (cast (And unit unit) _ a))).
287 interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r _ _ a).
288
289 (* ∨ introduction *)
290 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19 
291 for @{ 'Or_intro_l_ko_1 $a $ab }.
292 interpretation "Or_intro_l_ko_1" 'Or_intro_l_ko_1 a ab = 
293   (show ab (cast _ _ (Or_intro_l _ _ a))).
294
295 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19 
296 for @{ 'Or_intro_l_ko_2 $a $ab }.
297 interpretation "Or_intro_l_ko_2" 'Or_intro_l_ko_2 a ab = 
298   (cast _ _ (show ab (cast _ _ (Or_intro_l _ _ a)))).
299
300 notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))) (\vdots)" with precedence 19 
301 for @{ 'Or_intro_l_ok_1 $a $ab }.
302 interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab = 
303   (show ab (Or_intro_l _ _ a)).
304
305 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19 
306 for @{ 'Or_intro_l_ok_2 $a $ab }.
307 interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab = 
308   (cast _ _ (show ab (Or_intro_l _ _ a))).
309
310 notation > "∨_'i_l' term 90 a" with precedence 19
311 for @{ 'Or_intro_l (show $a ?) }.
312 interpretation "Or_intro_l KO" 'Or_intro_l a = (cast _ (Or _ unit) (Or_intro_l _ _ a)).
313 interpretation "Or_intro_l OK" 'Or_intro_l a = (Or_intro_l _ _ a). 
314   
315 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19 
316 for @{ 'Or_intro_r_ko_1 $a $ab }.
317 interpretation "Or_intro_r_ko_1" 'Or_intro_r_ko_1 a ab = 
318   (show ab (cast _ _ (Or_intro_r _ _ a))).
319
320 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19 
321 for @{ 'Or_intro_r_ko_2 $a $ab }.
322 interpretation "Or_intro_r_ko_2" 'Or_intro_r_ko_2 a ab = 
323   (cast _ _ (show ab (cast _ _ (Or_intro_r _ _ a)))).
324
325 notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))) (\vdots)" with precedence 19 
326 for @{ 'Or_intro_r_ok_1 $a $ab }.
327 interpretation "Or_intro_r_ok_1" 'Or_intro_r_ok_1 a ab = 
328   (show ab (Or_intro_r _ _ a)).
329
330 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\r))" with precedence 19 
331 for @{ 'Or_intro_r_ok_2 $a $ab }.
332 interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab = 
333   (cast _ _ (show ab (Or_intro_r _ _ a))).
334
335 notation > "∨_'i_r' term 90 a" with precedence 19
336 for @{ 'Or_intro_r (show $a ?) }.
337 interpretation "Or_intro_r KO" 'Or_intro_r a = (cast _ (Or unit _) (Or_intro_r _ _ a)).
338 interpretation "Or_intro_r OK" 'Or_intro_r a = (Or_intro_r _ _ a). 
339
340 (* ∨ elimination *)
341 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (mstyle color #ff0000 (∨\sub\e \emsp) ident Ha \emsp ident Hb)" with precedence 19
342 for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }.
343 interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc = 
344   (show c (cast _ _ (Or_elim _ _ _ (cast _ _ ab) (cast _ _ ac) (cast _ _ bc)))).
345
346 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∨\sub\e) \emsp ident Ha \emsp ident Hb)" with precedence 19
347 for @{ 'Or_elim_ko_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
348 interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c = 
349   (cast _ _ (show c (cast _ _ (Or_elim _ _ _ (cast _ _ ab) (cast _ _ ac) (cast _ _ bc))))).
350
351 notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)) (\vdots)" with precedence 19
352 for @{ 'Or_elim_ok_1 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
353 interpretation "Or_elim_ok_1" 'Or_elim_ok_1 ab \eta.ac \eta.bc c = 
354   (show c (Or_elim _ _ _ ab ac bc)).
355
356 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19
357 for @{ 'Or_elim_ok_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
358 interpretation "Or_elim_ok_2" 'Or_elim_ok_2 ab \eta.ac \eta.bc c = 
359   (cast _ _ (show c (Or_elim _ _ _ ab ac bc))).
360
361 definition unit_to ≝ λx:CProp.unit → x.
362
363 notation > "∨_'e' term 90 ab [ident Ha] term 90 cl [ident Hb] term 90 cr" with precedence 19
364 for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) }.
365 interpretation "Or_elim KO" 'Or_elim ab ac bc = 
366   (cast _ _ (Or_elim _ _ _ 
367     (cast (Or unit unit) _ ab) 
368     (cast (unit_to unit) (unit_to _) ac) 
369     (cast (unit_to unit) (unit_to _) bc))).
370 interpretation "Or_elim OK" 'Or_elim ab ac bc = (Or_elim _ _ _ ab ac bc).
371
372 (* ⊤ introduction *)
373 notation < "\infrule \nbsp ⊤ mstyle color #ff0000 (⊤\sub\i)" with precedence 19 
374 for @{'Top_intro_ko_1}.
375 interpretation "Top_intro_ko_1" 'Top_intro_ko_1 = 
376   (show _ (cast _ _ Top_intro)).
377
378 notation < "\infrule \nbsp mstyle color #ff0000 (⊤) mstyle color #ff0000 (⊤\sub\i)" with precedence 19 
379 for @{'Top_intro_ko_2}.
380 interpretation "Top_intro_ko_2" 'Top_intro_ko_2 = 
381   (cast _ _ (show _ (cast _ _ Top_intro))).
382
383 notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19 
384 for @{'Top_intro_ok_1}.
385 interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show _ Top_intro).
386
387 notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19 
388 for @{'Top_intro_ok_2 }.
389 interpretation "Top_intro_ok_2" 'Top_intro_ok_2 = (cast _ _ (show _ Top_intro)).
390
391 notation > "⊤_'i'" with precedence 19 for @{ 'Top_intro }.
392 interpretation "Top_intro KO" 'Top_intro = (cast _ _ Top_intro).
393 interpretation "Top_intro OK" 'Top_intro = Top_intro.
394
395 (* ⊥ introduction *)
396 notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19 
397 for @{'Bot_elim_ko_1 $a $b}.
398 interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b = 
399   (show a (Bot_elim _ (cast _ _ b))).
400
401 notation < "\infrule b mstyle color #ff0000 (a) mstyle color #ff0000 (⊥\sub\e)" with precedence 19 
402 for @{'Bot_elim_ko_2 $a $b}.
403 interpretation "Bot_elim_ko_2" 'Bot_elim_ko_2 a b = 
404   (cast _ _ (show a (Bot_elim _ (cast _ _ b)))).
405
406 notation < "maction (\infrule b a (⊥\sub\e)) (\vdots)" with precedence 19 
407 for @{'Bot_elim_ok_1 $a $b}.
408 interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b = 
409   (show a (Bot_elim _ b)).
410
411 notation < "\infrule b mstyle color #ff0000 (a) (⊥\sub\e)" with precedence 19 
412 for @{'Bot_elim_ok_2 $a $b}.
413 interpretation "Bot_elim_ok_2" 'Bot_elim_ok_2 a b = 
414   (cast _ _ (show a (Bot_elim _ b))).
415
416 notation > "⊥_'e' term 90 b" with precedence 19 
417 for @{ 'Bot_elim (show $b ?) }.
418 interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim _ (cast _ _ a)).  
419 interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim _ a).
420
421 (* ¬ introduction *)
422 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
423 for @{ 'Not_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
424 interpretation "Not_intro_ko_1" 'Not_intro_ko_1 ab \eta.b = 
425   (show ab (cast _ _ (Not_intro _ (cast _ _ b)))).
426
427 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
428 for @{ 'Not_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
429 interpretation "Not_intro_ko_2" 'Not_intro_ko_2 ab \eta.b = 
430   (cast _ _ (show ab (cast _ _ (Not_intro _ (cast _ _ b))))).
431
432 notation < "maction (\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\i) \emsp ident H) ) (\vdots)" with precedence 19
433 for @{ 'Not_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
434 interpretation "Not_intro_ok_1" 'Not_intro_ok_1 ab \eta.b = 
435   (show ab (Not_intro _ b)).
436
437 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub(\emsp\i) \emsp ident H) " with precedence 19
438 for @{ 'Not_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
439 interpretation "Not_intro_ok_2" 'Not_intro_ok_2 ab \eta.b = 
440   (cast _ _ (show ab (Not_intro _ b))).
441
442 notation > "¬_'i' [ident H] term 90 b" with precedence 19
443 for @{ 'Not_intro (λ${ident H}.show $b ?) }.
444 interpretation "Not_intro KO" 'Not_intro a = (cast _ _ (Not_intro _ (cast _ _ a))).
445 interpretation "Not_intro OK" 'Not_intro a = (Not_intro _ a).
446
447 (* ¬ elimination *)
448 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19 
449 for @{ 'Not_elim_ko_1 $ab $a $b }.
450 interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b = 
451   (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a)))).
452
453 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19 
454 for @{ 'Not_elim_ko_2 $ab $a $b }.
455 interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b = 
456   (cast _ _ (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a))))).
457
458 notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) ) (\vdots)" with precedence 19 
459 for @{ 'Not_elim_ok_1 $ab $a $b }.
460 interpretation "Not_elim_ok_1" 'Not_elim_ok_1 ab a b = 
461   (show b (Not_elim _ ab a)).
462
463 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (\lnot\sub(\emsp\e)) " with precedence 19 
464 for @{ 'Not_elim_ok_2 $ab $a $b }.
465 interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b = 
466   (cast _ _ (show b (Not_elim _ ab a))).
467
468 notation > "¬_'e' term 90 ab term 90 a" with precedence 19
469 for @{ 'Not_elim (show $ab ?) (show $a ?) }.
470 interpretation "Not_elim KO" 'Not_elim ab a = 
471   (cast _ _ (Not_elim unit (cast _ _ ab) (cast _ _ a))).
472 interpretation "Not_elim OK" 'Not_elim ab a = 
473   (Not_elim _ ab a).
474
475 (* RAA *)
476 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
477 for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
478 interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn = 
479   (show Pn (cast _ _ (Raa _ (cast _ _ Px)))).
480
481 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
482 for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
483 interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn = 
484   (cast _ _ (show Pn (cast _ _ (Raa _ (cast _ _ Px))))).
485
486 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)) (\vdots)" with precedence 19
487 for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
488 interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn = 
489   (show Pn (Raa _ Px)).
490
491 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (\RAA \emsp ident x)" with precedence 19
492 for @{ 'RAA_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
493 interpretation "RAA_ok_2" 'RAA_ok_2 Px Pn = 
494   (cast _ _ (show Pn (Raa _ Px))).
495
496 notation > "'RAA' [ident H] term 90 b" with precedence 19 
497 for @{ 'Raa (λ${ident H}.show $b ?) }. 
498 interpretation "RAA KO" 'Raa p = (cast _ unit (Raa _ (cast _ (unit_to _) p))).
499 interpretation "RAA OK" 'Raa p = (Raa _ p).
500
501 (* ∃ introduction *)
502 notation < "\infrule hbox(\emsp Pn \emsp) Px mstyle color #ff0000 (∃\sub\i)" with precedence 19
503 for @{ 'Exists_intro_ko_1 $Pn $Px }.
504 interpretation "Exists_intro_ko_1" 'Exists_intro_ko_1 Pn Px = 
505   (show Px (cast _ _ (Exists_intro _ _ _ (cast _ _ Pn)))).
506
507 notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) mstyle color #ff0000 (∃\sub\i)" with precedence 19
508 for @{ 'Exists_intro_ko_2 $Pn $Px }.
509 interpretation "Exists_intro_ko_2" 'Exists_intro_ko_2 Pn Px = 
510   (cast _ _ (show Px (cast _ _ (Exists_intro _ _ _ (cast _ _ Pn))))).
511
512 notation < "maction (\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)) (\vdots)" with precedence 19
513 for @{ 'Exists_intro_ok_1 $Pn $Px }.
514 interpretation "Exists_intro_ok_1" 'Exists_intro_ok_1 Pn Px = 
515   (show Px (Exists_intro _ _ _ Pn)).
516
517 notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) (∃\sub\i)" with precedence 19
518 for @{ 'Exists_intro_ok_2 $Pn $Px }.
519 interpretation "Exists_intro_ok_2" 'Exists_intro_ok_2 Pn Px = 
520   (cast _ _ (show Px (Exists_intro _ _ _ Pn))).
521
522 notation >"∃_'i' {term 90 t} term 90 Pt" non associative with precedence 19
523 for @{'Exists_intro $t (λw.? w) (show $Pt ?)}. 
524 interpretation "Exists_intro KO" 'Exists_intro t P Pt =
525  (cast _ _ (Exists_intro sort P t (cast _ _ Pt))).
526 interpretation "Exists_intro OK" 'Exists_intro t P Pt =
527  (Exists_intro sort P t Pt).
528  
529 (* ∃ elimination *)
530 notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (mstyle color #ff0000 (∃\sub\e) \emsp ident n \emsp ident HPn)" with precedence 19
531 for @{ 'Exists_elim_ko_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
532 interpretation "Exists_elim_ko_1" 'Exists_elim_ko_1 ExPx Pc c =
533     (show c (cast _ _ (Exists_elim _ _ _ (cast _ _ ExPx) (cast _ _ Pc)))).
534
535 notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∃\sub\e) \emsp ident n \emsp ident HPn)" with precedence 19
536 for @{ 'Exists_elim_ko_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
537 interpretation "Exists_elim_ko_2" 'Exists_elim_ko_2 ExPx Pc c =
538     (cast _ _ (show c (cast _ _ (Exists_elim _ _ _ (cast _ _ ExPx) (cast _ _ Pc))))).
539
540 notation < "maction (\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)) (\vdots)" with precedence 19
541 for @{ 'Exists_elim_ok_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
542 interpretation "Exists_elim_ok_1" 'Exists_elim_ok_1 ExPx Pc c =
543     (show c (Exists_elim _ _ _ ExPx Pc)).
544
545 notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) mstyle color #ff0000 (c) (∃\sub\e \emsp ident n \emsp ident HPn)" with precedence 19
546 for @{ 'Exists_elim_ok_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
547 interpretation "Exists_elim_ok_2" 'Exists_elim_ok_2 ExPx Pc c =
548     (cast _ _ (show c (Exists_elim _ _ _ ExPx Pc))).
549
550 definition ex_concl := λx:sort → CProp.∀y:sort.unit → x y.
551 definition ex_concl_dummy := ∀y:sort.unit → unit.
552 definition fake_pred := λx:sort.unit.
553
554 notation >"∃_'e' term 90 ExPt {ident t} [ident H] term 90 c" non associative with precedence 19
555 for @{'Exists_elim (λx.? x) (show $ExPt ?) (λ${ident t}:sort.λ${ident H}.show $c ?)}. 
556 interpretation "Exists_elim KO" 'Exists_elim P ExPt c =
557  (cast _ _ (Exists_elim sort P _ 
558    (cast (Exists _ P)  _ ExPt) 
559    (cast ex_concl_dummy (ex_concl _) c))).
560 interpretation "Exists_elim OK" 'Exists_elim P ExPt c =
561  (Exists_elim sort P _ ExPt c).
562
563 (* ∀ introduction *)
564
565 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19
566 for @{ 'Forall_intro_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
567 interpretation "Forall_intro_ko_1" 'Forall_intro_ko_1 Px Pn = 
568   (show Pn (cast _ _ (Forall_intro _ _ (cast _ _ Px)))).
569
570 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19
571 for @{ 'Forall_intro_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
572 interpretation "Forall_intro_ko_2" 'Forall_intro_ko_2 Px Pn = 
573   (cast _ _ (show Pn (cast _ _ (Forall_intro _ _ (cast _ _ Px))))).
574
575 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)) (\vdots)" with precedence 19
576 for @{ 'Forall_intro_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
577 interpretation "Forall_intro_ok_1" 'Forall_intro_ok_1 Px Pn = 
578   (show Pn (Forall_intro _ _ Px)).
579
580 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\i \emsp ident x)" with precedence 19
581 for @{ 'Forall_intro_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
582 interpretation "Forall_intro_ok_2" 'Forall_intro_ok_2 Px Pn = 
583   (cast _ _ (show Pn (Forall_intro _ _ Px))).
584
585 notation > "∀_'i' {ident y} term 90 Px" non associative with precedence 19
586 for @{ 'Forall_intro (λ_.?) (λ${ident y}.show $Px ?) }. 
587 interpretation "Forall_intro KO" 'Forall_intro P Px =
588   (cast _ _ (Forall_intro sort P (cast _ _ Px))). 
589 interpretation "Forall_intro OK" 'Forall_intro P Px =
590   (Forall_intro sort P Px). 
591
592 (* ∀ elimination *)
593 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\e))" with precedence 19
594 for @{ 'Forall_elim_ko_1 $Px $Pn }.
595 interpretation "Forall_elim_ko_1" 'Forall_elim_ko_1 Px Pn = 
596   (show Pn (cast _ _ (Forall_elim _ _ _ (cast _ _ Px)))).
597
598 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\e))" with precedence 19
599 for @{ 'Forall_elim_ko_2 $Px $Pn }.
600 interpretation "Forall_elim_ko_2" 'Forall_elim_ko_2 Px Pn = 
601   (cast _ _ (show Pn (cast _ _ (Forall_elim _ _ _ (cast _ _ Px))))).
602
603 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\e)) (\vdots)" with precedence 19
604 for @{ 'Forall_elim_ok_1 $Px $Pn }.
605 interpretation "Forall_elim_ok_1" 'Forall_elim_ok_1 Px Pn = 
606   (show Pn (Forall_elim _ _ _ Px)).
607
608 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\e)" with precedence 19
609 for @{ 'Forall_elim_ok_2 $Px $Pn }.
610 interpretation "Forall_elim_ok_2" 'Forall_elim_ok_2 Px Pn = 
611   (cast _ _ (show Pn (Forall_elim _ _ _ Px))).
612
613 notation > "∀_'e' {term 90 t} term 90 Pn" non associative with precedence 19
614 for @{ 'Forall_elim (λ_.?) $t (show $Pn ?) }. 
615 interpretation "Forall_elim KO" 'Forall_elim P t Px =
616   (cast _ unit (Forall_elim sort P t (cast _ _ Px))). 
617 interpretation "Forall_elim OK" 'Forall_elim P t Px =
618   (Forall_elim sort P t Px). 
619
620 (* already proved lemma *)
621 definition hide_args : ∀A:Type.∀a:A.A := λA:Type.λa:A.a.
622 notation < "t" non associative with precedence 90 for @{'hide_args $t}.
623 interpretation "hide 0 args"  'hide_args t = (hide_args _ t).
624 interpretation "hide 1 args"  'hide_args t = (hide_args _ t _).
625 interpretation "hide 2 args"  'hide_args t = (hide_args _ t _ _).
626 interpretation "hide 3 args"  'hide_args t = (hide_args _ t _ _ _).
627 interpretation "hide 4 args"  'hide_args t = (hide_args _ t _ _ _ _). 
628 interpretation "hide 5 args"  'hide_args t = (hide_args _ t _ _ _ _ _).
629 interpretation "hide 6 args"  'hide_args t = (hide_args _ t _ _ _ _ _ _).
630 interpretation "hide 7 args"  'hide_args t = (hide_args _ t _ _ _ _ _ _ _).
631
632 (* more args crashes the pattern matcher *)
633
634 (* already proved lemma, 0 assumptions *)
635 definition Lemma : ΠA.A→A ≝ λA:CProp.λa:A.a.
636
637 notation < "\infrule 
638          (\infrule 
639              (\emsp) 
640              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
641          p \nbsp" 
642 non associative with precedence 19
643 for @{ 'lemma_ko_1 $p ($H : $_) }.
644 interpretation "lemma_ko_1" 'lemma_ko_1 p H = 
645   (show p (cast _ _ (Lemma _ (cast _ _ H)))). 
646
647 notation < "\infrule 
648          (\infrule 
649              (\emsp) 
650              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
651          mstyle color #ff0000 (p) \nbsp" 
652 non associative with precedence 19
653 for @{ 'lemma_ko_2 $p ($H : $_) }.
654 interpretation "lemma_ko_2" 'lemma_ko_2 p H = 
655   (cast _ _ (show p (cast _ _ 
656     (Lemma _ (cast _ _ H))))). 
657
658
659 notation < "\infrule 
660          (\infrule 
661              (\emsp) 
662              (╲ mstyle mathsize normal (H) ╱) \nbsp) 
663          p \nbsp" 
664 non associative with precedence 19
665 for @{ 'lemma_ok_1 $p ($H : $_) }.
666 interpretation "lemma_ok_1" 'lemma_ok_1 p H = 
667   (show p (Lemma _ H)). 
668
669 notation < "\infrule 
670          (\infrule 
671              (\emsp) 
672              (╲ mstyle mathsize normal (H) ╱) \nbsp) 
673          mstyle color #ff0000 (p) \nbsp" 
674 non associative with precedence 19
675 for @{ 'lemma_ok_2 $p ($H : $_) }.
676 interpretation "lemma_ok_2" 'lemma_ok_2 p H = 
677   (cast _ _ (show p (Lemma _ H))). 
678
679 notation > "'lem' 0 term 90 l" non associative with precedence 19
680 for @{ 'Lemma (hide_args ? $l : ?) }.
681 interpretation "lemma KO" 'Lemma l = 
682   (cast _ _ (Lemma unit (cast unit _ l))). 
683 interpretation "lemma OK" 'Lemma l = (Lemma _ l).
684
685
686 (* already proved lemma, 1 assumption *)
687 definition Lemma1 : ΠA,B. (A ⇒ B) → A → B ≝ 
688  λA,B:CProp.λf:A⇒B.λa:A.
689   Imply_elim A B f a.
690
691 notation < "\infrule 
692          (\infrule 
693              (\emsp a \emsp) 
694              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
695          p \nbsp" 
696 non associative with precedence 19
697 for @{ 'lemma1_ko_1 $a $p ($H : $_) }.
698 interpretation "lemma1_ko_1" 'lemma1_ko_1 a p H = 
699   (show p (cast _ _ (Lemma1 _ _ (cast _ _ H) (cast _ _ a)))). 
700
701 notation < "\infrule 
702          (\infrule 
703              (\emsp a \emsp) 
704              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
705          mstyle color #ff0000 (p) \nbsp" 
706 non associative with precedence 19
707 for @{ 'lemma1_ko_2 $a $p ($H : $_) }.
708 interpretation "lemma1_ko_2" 'lemma1_ko_2 a p H = 
709   (cast _ _ (show p (cast _ _ 
710     (Lemma1 _ _ (cast _ _ H) (cast _ _ a))))). 
711
712
713 notation < "\infrule 
714          (\infrule 
715              (\emsp a \emsp) 
716              (╲ mstyle mathsize normal (H) ╱) \nbsp) 
717          p \nbsp" 
718 non associative with precedence 19
719 for @{ 'lemma1_ok_1 $a $p ($H : $_) }.
720 interpretation "lemma1_ok_1" 'lemma1_ok_1 a p H = 
721   (show p (Lemma1 _ _ H a)). 
722
723 notation < "\infrule 
724          (\infrule 
725              (\emsp a \emsp) 
726              (╲ mstyle mathsize normal (H) ╱) \nbsp) 
727          mstyle color #ff0000 (p) \nbsp" 
728 non associative with precedence 19
729 for @{ 'lemma1_ok_2 $a $p ($H : $_) }.
730 interpretation "lemma1_ok_2" 'lemma1_ok_2 a p H = 
731   (cast _ _ (show p (Lemma1 _ _ H a))). 
732
733
734 notation > "'lem' 1 term 90 l term 90 p" non associative with precedence 19
735 for @{ 'Lemma1 (hide_args ? $l : ?) (show $p ?) }.
736 interpretation "lemma 1 KO" 'Lemma1 l p = 
737   (cast _ _ (Lemma1 unit unit (cast (Imply unit unit) _ l) (cast unit _ p))). 
738 interpretation "lemma 1 OK" 'Lemma1 l p = (Lemma1 _ _ l p).
739
740 (* already proved lemma, 2 assumptions *)
741 definition Lemma2 : ΠA,B,C. (A ⇒ B ⇒ C) → A → B → C ≝ 
742  λA,B,C:CProp.λf:A⇒B⇒C.λa:A.λb:B.
743   Imply_elim B C (Imply_elim A (B⇒C) f a) b.
744
745 notation < "\infrule 
746          (\infrule 
747              (\emsp a \emsp\emsp\emsp b \emsp) 
748              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
749          p \nbsp" 
750 non associative with precedence 19
751 for @{ 'lemma2_ko_1 $a $b $p ($H : $_) }.
752 interpretation "lemma2_ko_1" 'lemma2_ko_1 a b p H = 
753   (show p (cast _ _ (Lemma2 _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b)))). 
754
755 notation < "\infrule 
756          (\infrule 
757              (\emsp a \emsp\emsp\emsp b \emsp) 
758              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
759          mstyle color #ff0000 (p) \nbsp" 
760 non associative with precedence 19
761 for @{ 'lemma2_ko_2 $a $b $p ($H : $_) }.
762 interpretation "lemma2_ko_2" 'lemma2_ko_2 a b p H = 
763   (cast _ _ (show p (cast _ _ 
764     (Lemma2 _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b))))). 
765
766
767 notation < "\infrule 
768          (\infrule 
769              (\emsp a \emsp\emsp\emsp b \emsp) 
770              (╲ mstyle mathsize normal (H) ╱) \nbsp) 
771          p \nbsp" 
772 non associative with precedence 19
773 for @{ 'lemma2_ok_1 $a $b $p ($H : $_) }.
774 interpretation "lemma2_ok_1" 'lemma2_ok_1 a b p H = 
775   (show p (Lemma2 _ _ _ H a b)). 
776
777 notation < "\infrule 
778          (\infrule 
779              (\emsp a \emsp\emsp\emsp b \emsp) 
780              (╲ mstyle mathsize normal (H) ╱) \nbsp) 
781          mstyle color #ff0000 (p) \nbsp" 
782 non associative with precedence 19
783 for @{ 'lemma2_ok_2 $a $b $p ($H : $_) }.
784 interpretation "lemma2_ok_2" 'lemma2_ok_2 a b p H = 
785   (cast _ _ (show p (Lemma2 _ _ _ H a b))). 
786
787 notation > "'lem' 2 term 90 l term 90 p term 90 q" non associative with precedence 19
788 for @{ 'Lemma2 (hide_args ? $l : ?) (show $p ?) (show $q ?) }.
789 interpretation "lemma 2 KO" 'Lemma2 l p q = 
790   (cast _ _ (Lemma2 unit unit unit (cast (Imply unit (Imply unit unit)) _ l) (cast unit _ p) (cast unit _ q))). 
791 interpretation "lemma 2 OK" 'Lemma2 l p q = (Lemma2 _ _ _ l p q).
792
793 (* already proved lemma, 3 assumptions *)
794 definition Lemma3 : ΠA,B,C,D. (A ⇒ B ⇒ C ⇒ D) → A → B → C → D ≝ 
795  λA,B,C,D:CProp.λf:A⇒B⇒C⇒D.λa:A.λb:B.λc:C.
796   Imply_elim C D (Imply_elim B (C⇒D) (Imply_elim A (B⇒C⇒D) f a) b) c.
797
798 notation < "\infrule 
799          (\infrule 
800              (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) 
801              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
802          p \nbsp" 
803 non associative with precedence 19
804 for @{ 'lemma3_ko_1 $a $b $c $p ($H : $_) }.
805 interpretation "lemma3_ko_1" 'lemma3_ko_1 a b c p H = 
806   (show p (cast _ _ 
807    (Lemma3 _ _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b) (cast _ _ c)))). 
808
809 notation < "\infrule 
810          (\infrule 
811              (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) 
812              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
813          mstyle color #ff0000 (p) \nbsp" 
814 non associative with precedence 19
815 for @{ 'lemma3_ko_2 $a $b $c $p ($H : $_) }.
816 interpretation "lemma3_ko_2" 'lemma3_ko_2 a b c p H = 
817   (cast _ _ (show p (cast _ _ 
818     (Lemma3 _ _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b) (cast _ _ c))))). 
819
820
821 notation < "\infrule 
822          (\infrule 
823              (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) 
824              (╲ mstyle mathsize normal (H) ╱) \nbsp) 
825          p \nbsp" 
826 non associative with precedence 19
827 for @{ 'lemma3_ok_1 $a $b $c $p ($H : $_) }.
828 interpretation "lemma3_ok_1" 'lemma3_ok_1 a b c p H = 
829   (show p (Lemma3 _ _ _ _ H a b c)). 
830
831 notation < "\infrule 
832          (\infrule 
833              (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) 
834              (╲ mstyle mathsize normal (H) ╱) \nbsp) 
835          mstyle color #ff0000 (p) \nbsp" 
836 non associative with precedence 19
837 for @{ 'lemma3_ok_2 $a $b $c $p ($H : $_) }.
838 interpretation "lemma3_ok_2" 'lemma3_ok_2 a b c p H = 
839   (cast _ _ (show p (Lemma3 _ _ _ _ H a b c))). 
840
841 notation > "'lem' 3 term 90 l term 90 p term 90 q term 90 r" non associative with precedence 19
842 for @{ 'Lemma3 (hide_args ? $l : ?) (show $p ?) (show $q ?) (show $r ?) }.
843 interpretation "lemma 3 KO" 'Lemma3 l p q r = 
844   (cast _ _ (Lemma3 unit unit unit unit (cast (Imply unit (Imply unit (Imply unit unit))) _ l) (cast unit _ p) (cast unit _ q) (cast unit _ r))). 
845 interpretation "lemma 3 OK" 'Lemma3 l p q r = (Lemma3 _ _ _ _ l p q r).