helm/software/matita/library/didactic/support/natural_deduction.ma

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