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
 194 interpretation "Imply_intro KO" 'Imply_intro b pb =
 195   (cast ? (Imply unit b) (Imply_intro ? b pb)).
 196 interpretation "Imply_intro OK" 'Imply_intro b pb =
 197   (Imply_intro ? b pb).
 198
 199 (* ⇒ elimination *)
 200 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19
 201 for @{ 'Imply_elim_ko_1 $ab $a $b }.
 202 interpretation "Imply_elim_ko_1" 'Imply_elim_ko_1 ab a b =
 203   (show b (cast ? ? (Imply_elim ? ? (cast ? ? ab) (cast ? ? a)))).
 204
 205 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19
 206 for @{ 'Imply_elim_ko_2 $ab $a $b }.
 207 interpretation "Imply_elim_ko_2" 'Imply_elim_ko_2 ab a b =
 208   (cast ? ? (show b (cast ? ? (Imply_elim ? ? (cast ? ? ab) (cast ? ? a))))).
 209
 210 notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) ) (\vdots)" with precedence 19
 211 for @{ 'Imply_elim_ok_1 $ab $a $b }.
 212 interpretation "Imply_elim_ok_1" 'Imply_elim_ok_1 ab a b =
 213   (show b (Imply_elim ? ? ab a)).
 214
 215 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (⇒\sub\e) " with precedence 19
 216 for @{ 'Imply_elim_ok_2 $ab $a $b }.
 217 interpretation "Imply_elim_ok_2" 'Imply_elim_ok_2 ab a b =
 218   (cast ? ? (show b (Imply_elim ? ? ab a))).
 219
 220 notation > "⇒#'e' term 90 ab term 90 a" with precedence 19
 221 for @{ 'Imply_elim (show $ab ?) (show $a ?) }.
 222 interpretation "Imply_elim KO" 'Imply_elim ab a =
 223   (cast ? ? (Imply_elim ? ? (cast (Imply unit unit) ? ab) (cast unit ? a))).
 224 interpretation "Imply_elim OK" 'Imply_elim ab a =
 225   (Imply_elim ? ? ab a).
 226
 227 (* ∧ introduction *)
 228 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19
 229 for @{ 'And_intro_ko_1 $a $b $ab }.
 230 interpretation "And_intro_ko_1" 'And_intro_ko_1 a b ab =
 231   (show ab (cast ? ? (And_intro ? ? a b))).
 232
 233 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19
 234 for @{ 'And_intro_ko_2 $a $b $ab }.
 235 interpretation "And_intro_ko_2" 'And_intro_ko_2 a b ab =
 236   (cast ? ? (show ab (cast ? ? (And_intro ? ? a b)))).
 237
 238 notation < "maction (\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)) (\vdots)" with precedence 19
 239 for @{ 'And_intro_ok_1 $a $b $ab }.
 240 interpretation "And_intro_ok_1" 'And_intro_ok_1 a b ab =
 241   (show ab (And_intro ? ? a b)).
 242
 243 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) (∧\sub\i)" with precedence 19
 244 for @{ 'And_intro_ok_2 $a $b $ab }.
 245 interpretation "And_intro_ok_2" 'And_intro_ok_2 a b ab =
 246   (cast ? ? (show ab (And_intro ? ? a b))).
 247
 248 notation > "∧#'i' term 90 a term 90 b" with precedence 19
 249 for @{ 'And_intro (show $a ?) (show $b ?) }.
 250 interpretation "And_intro KO" 'And_intro a b = (cast ? ? (And_intro ? ? a b)).
 251 interpretation "And_intro OK" 'And_intro a b = (And_intro ? ? a b).
 252
 253 (* ∧ elimination *)
 254 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19
 255 for @{ 'And_elim_l_ko_1 $ab $a }.
 256 interpretation "And_elim_l_ko_1" 'And_elim_l_ko_1 ab a =
 257   (show a (cast ? ? (And_elim_l ? ? (cast ? ? ab)))).
 258
 259 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19
 260 for @{ 'And_elim_l_ko_2 $ab $a }.
 261 interpretation "And_elim_l_ko_2" 'And_elim_l_ko_2 ab a =
 262   (cast ? ? (show a (cast ? ? (And_elim_l ? ? (cast ? ? ab))))).
 263
 264 notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))) (\vdots)" with precedence 19
 265 for @{ 'And_elim_l_ok_1 $ab $a }.
 266 interpretation "And_elim_l_ok_1" 'And_elim_l_ok_1 ab a =
 267   (show a (And_elim_l ? ? ab)).
 268
 269 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\l))" with precedence 19
 270 for @{ 'And_elim_l_ok_2 $ab $a }.
 271 interpretation "And_elim_l_ok_2" 'And_elim_l_ok_2 ab a =
 272   (cast ? ? (show a (And_elim_l ? ? ab))).
 273
 274 notation > "∧#'e_l' term 90 ab" with precedence 19
 275 for @{ 'And_elim_l (show $ab ?) }.
 276 interpretation "And_elim_l KO" 'And_elim_l a = (cast ? ? (And_elim_l ? ? (cast (And unit unit) ? a))).
 277 interpretation "And_elim_l OK" 'And_elim_l a = (And_elim_l ? ? a).
 278
 279 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19
 280 for @{ 'And_elim_r_ko_1 $ab $a }.
 281 interpretation "And_elim_r_ko_1" 'And_elim_r_ko_1 ab a =
 282   (show a (cast ? ? (And_elim_r ? ? (cast ? ? ab)))).
 283
 284 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19
 285 for @{ 'And_elim_r_ko_2 $ab $a }.
 286 interpretation "And_elim_r_ko_2" 'And_elim_r_ko_2 ab a =
 287   (cast ? ? (show a (cast ? ? (And_elim_r ? ? (cast ? ? ab))))).
 288
 289 notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))) (\vdots)" with precedence 19
 290 for @{ 'And_elim_r_ok_1 $ab $a }.
 291 interpretation "And_elim_r_ok_1" 'And_elim_r_ok_1 ab a =
 292   (show a (And_elim_r ? ? ab)).
 293
 294 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\r))" with precedence 19
 295 for @{ 'And_elim_r_ok_2 $ab $a }.
 296 interpretation "And_elim_r_ok_2" 'And_elim_r_ok_2 ab a =
 297   (cast ? ? (show a (And_elim_r ? ? ab))).
 298
 299 notation > "∧#'e_r' term 90 ab" with precedence 19
 300 for @{ 'And_elim_r (show $ab ?) }.
 301 interpretation "And_elim_r KO" 'And_elim_r a = (cast ? ? (And_elim_r ? ? (cast (And unit unit) ? a))).
 302 interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r ? ? a).
 303
 304 (* ∨ introduction *)
 305 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19
 306 for @{ 'Or_intro_l_ko_1 $a $ab }.
 307 interpretation "Or_intro_l_ko_1" 'Or_intro_l_ko_1 a ab =
 308   (show ab (cast ? ? (Or_intro_l ? ? a))).
 309
 310 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19
 311 for @{ 'Or_intro_l_ko_2 $a $ab }.
 312 interpretation "Or_intro_l_ko_2" 'Or_intro_l_ko_2 a ab =
 313   (cast ? ? (show ab (cast ? ? (Or_intro_l ? ? a)))).
 314
 315 notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))) (\vdots)" with precedence 19
 316 for @{ 'Or_intro_l_ok_1 $a $ab }.
 317 interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab =
 318   (show ab (Or_intro_l ? ? a)).
 319
 320 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19
 321 for @{ 'Or_intro_l_ok_2 $a $ab }.
 322 interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab =
 323   (cast ? ? (show ab (Or_intro_l ? ? a))).
 324
 325 notation > "∨#'i_l' term 90 a" with precedence 19
 326 for @{ 'Or_intro_l (show $a ?) }.
 327 interpretation "Or_intro_l KO" 'Or_intro_l a = (cast ? (Or ? unit) (Or_intro_l ? ? a)).
 328 interpretation "Or_intro_l OK" 'Or_intro_l a = (Or_intro_l ? ? a).
 329
 330 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19
 331 for @{ 'Or_intro_r_ko_1 $a $ab }.
 332 interpretation "Or_intro_r_ko_1" 'Or_intro_r_ko_1 a ab =
 333   (show ab (cast ? ? (Or_intro_r ? ? a))).
 334
 335 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19
 336 for @{ 'Or_intro_r_ko_2 $a $ab }.
 337 interpretation "Or_intro_r_ko_2" 'Or_intro_r_ko_2 a ab =
 338   (cast ? ? (show ab (cast ? ? (Or_intro_r ? ? a)))).
 339
 340 notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))) (\vdots)" with precedence 19
 341 for @{ 'Or_intro_r_ok_1 $a $ab }.
 342 interpretation "Or_intro_r_ok_1" 'Or_intro_r_ok_1 a ab =
 343   (show ab (Or_intro_r ? ? a)).
 344
 345 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\r))" with precedence 19
 346 for @{ 'Or_intro_r_ok_2 $a $ab }.
 347 interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab =
 348   (cast ? ? (show ab (Or_intro_r ? ? a))).
 349
 350 notation > "∨#'i_r' term 90 a" with precedence 19
 351 for @{ 'Or_intro_r (show $a ?) }.
 352 interpretation "Or_intro_r KO" 'Or_intro_r a = (cast ? (Or unit ?) (Or_intro_r ? ? a)).
 353 interpretation "Or_intro_r OK" 'Or_intro_r a = (Or_intro_r ? ? a).
 354
 355 (* ∨ elimination *)
 356 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
 357 for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }.
 358 interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc =
 359   (show c (cast ? ? (Or_elim ? ? ? (cast ? ? ab) (cast ? ? ac) (cast ? ? bc)))).
 360
 361 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
 362 for @{ 'Or_elim_ko_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 363 interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c =
 364   (cast ? ? (show c (cast ? ? (Or_elim ? ? ? (cast ? ? ab) (cast ? ? ac) (cast ? ? bc))))).
 365
 366 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
 367 for @{ 'Or_elim_ok_1 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 368 interpretation "Or_elim_ok_1" 'Or_elim_ok_1 ab \eta.ac \eta.bc c =
 369   (show c (Or_elim ? ? ? ab ac bc)).
 370
 371 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
 372 for @{ 'Or_elim_ok_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 373 interpretation "Or_elim_ok_2" 'Or_elim_ok_2 ab \eta.ac \eta.bc c =
 374   (cast ? ? (show c (Or_elim ? ? ? ab ac bc))).
 375
 376 definition unit_to ≝ λx:CProp.unit → x.
 377
 378 notation > "∨#'e' term 90 ab [ident Ha] term 90 cl [ident Hb] term 90 cr" with precedence 19
 379 for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) }.
 380 interpretation "Or_elim KO" 'Or_elim ab ac bc =
 381   (cast ? ? (Or_elim ? ? ?
 382     (cast (Or unit unit) ? ab)
 383     (cast (unit_to unit) (unit_to ?) ac)
 384     (cast (unit_to unit) (unit_to ?) bc))).
 385 interpretation "Or_elim OK" 'Or_elim ab ac bc = (Or_elim ? ? ? ab ac bc).
 386
 387 (* ⊤ introduction *)
 388 notation < "\infrule \nbsp ⊤ mstyle color #ff0000 (⊤\sub\i)" with precedence 19
 389 for @{'Top_intro_ko_1}.
 390 interpretation "Top_intro_ko_1" 'Top_intro_ko_1 =
 391   (show ? (cast ? ? Top_intro)).
 392
 393 notation < "\infrule \nbsp mstyle color #ff0000 (⊤) mstyle color #ff0000 (⊤\sub\i)" with precedence 19
 394 for @{'Top_intro_ko_2}.
 395 interpretation "Top_intro_ko_2" 'Top_intro_ko_2 =
 396   (cast ? ? (show ? (cast ? ? Top_intro))).
 397
 398 notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19
 399 for @{'Top_intro_ok_1}.
 400 interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show ? Top_intro).
 401
 402 notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19
 403 for @{'Top_intro_ok_2 }.
 404 interpretation "Top_intro_ok_2" 'Top_intro_ok_2 = (cast ? ? (show ? Top_intro)).
 405
 406 notation > "⊤#'i'" with precedence 19 for @{ 'Top_intro }.
 407 interpretation "Top_intro KO" 'Top_intro = (cast ? ? Top_intro).
 408 interpretation "Top_intro OK" 'Top_intro = Top_intro.
 409
 410 (* ⊥ introduction *)
 411 notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19
 412 for @{'Bot_elim_ko_1 $a $b}.
 413 interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b =
 414   (show a (Bot_elim ? (cast ? ? b))).
 415
 416 notation < "\infrule b mstyle color #ff0000 (a) mstyle color #ff0000 (⊥\sub\e)" with precedence 19
 417 for @{'Bot_elim_ko_2 $a $b}.
 418 interpretation "Bot_elim_ko_2" 'Bot_elim_ko_2 a b =
 419   (cast ? ? (show a (Bot_elim ? (cast ? ? b)))).
 420
 421 notation < "maction (\infrule b a (⊥\sub\e)) (\vdots)" with precedence 19
 422 for @{'Bot_elim_ok_1 $a $b}.
 423 interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b =
 424   (show a (Bot_elim ? b)).
 425
 426 notation < "\infrule b mstyle color #ff0000 (a) (⊥\sub\e)" with precedence 19
 427 for @{'Bot_elim_ok_2 $a $b}.
 428 interpretation "Bot_elim_ok_2" 'Bot_elim_ok_2 a b =
 429   (cast ? ? (show a (Bot_elim ? b))).
 430
 431 notation > "⊥#'e' term 90 b" with precedence 19
 432 for @{ 'Bot_elim (show $b ?) }.
 433 interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim ? (cast ? ? a)).
 434 interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim ? a).
 435
 436 (* ¬ introduction *)
 437 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
 438 for @{ 'Not_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
 439 interpretation "Not_intro_ko_1" 'Not_intro_ko_1 ab \eta.b =
 440   (show ab (cast ? ? (Not_intro ? (cast ? ? b)))).
 441
 442 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
 443 for @{ 'Not_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
 444 interpretation "Not_intro_ko_2" 'Not_intro_ko_2 ab \eta.b =
 445   (cast ? ? (show ab (cast ? ? (Not_intro ? (cast ? ? b))))).
 446
 447 notation < "maction (\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\i) \emsp ident H) ) (\vdots)" with precedence 19
 448 for @{ 'Not_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
 449 interpretation "Not_intro_ok_1" 'Not_intro_ok_1 ab \eta.b =
 450   (show ab (Not_intro ? b)).
 451
 452 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub(\emsp\i) \emsp ident H) " with precedence 19
 453 for @{ 'Not_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
 454 interpretation "Not_intro_ok_2" 'Not_intro_ok_2 ab \eta.b =
 455   (cast ? ? (show ab (Not_intro ? b))).
 456
 457 notation > "¬#'i' [ident H] term 90 b" with precedence 19
 458 for @{ 'Not_intro (λ${ident H}.show $b ?) }.
 459 interpretation "Not_intro KO" 'Not_intro a = (cast ? ? (Not_intro ? (cast ? ? a))).
 460 interpretation "Not_intro OK" 'Not_intro a = (Not_intro ? a).
 461
 462 (* ¬ elimination *)
 463 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19
 464 for @{ 'Not_elim_ko_1 $ab $a $b }.
 465 interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b =
 466   (show b (cast ? ? (Not_elim ? (cast ? ? ab) (cast ? ? a)))).
 467
 468 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19
 469 for @{ 'Not_elim_ko_2 $ab $a $b }.
 470 interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b =
 471   (cast ? ? (show b (cast ? ? (Not_elim ? (cast ? ? ab) (cast ? ? a))))).
 472
 473 notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) ) (\vdots)" with precedence 19
 474 for @{ 'Not_elim_ok_1 $ab $a $b }.
 475 interpretation "Not_elim_ok_1" 'Not_elim_ok_1 ab a b =
 476   (show b (Not_elim ? ab a)).
 477
 478 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (\lnot\sub(\emsp\e)) " with precedence 19
 479 for @{ 'Not_elim_ok_2 $ab $a $b }.
 480 interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b =
 481   (cast ? ? (show b (Not_elim ? ab a))).
 482
 483 notation > "¬#'e' term 90 ab term 90 a" with precedence 19
 484 for @{ 'Not_elim (show $ab ?) (show $a ?) }.
 485 interpretation "Not_elim KO" 'Not_elim ab a =
 486   (cast ? ? (Not_elim unit (cast ? ? ab) (cast ? ? a))).
 487 interpretation "Not_elim OK" 'Not_elim ab a =
 488   (Not_elim ? ab a).
 489
 490 (* RAA *)
 491 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
 492 for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
 493 interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn =
 494   (show Pn (cast ? ? (Raa ? (cast ? ? Px)))).
 495
 496 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
 497 for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
 498 interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn =
 499   (cast ? ? (show Pn (cast ? ? (Raa ? (cast ? ? Px))))).
 500
 501 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)) (\vdots)" with precedence 19
 502 for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
 503 interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn =
 504   (show Pn (Raa ? Px)).
 505
 506 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (\RAA \emsp ident x)" with precedence 19
 507 for @{ 'RAA_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
 508 interpretation "RAA_ok_2" 'RAA_ok_2 Px Pn =
 509   (cast ? ? (show Pn (Raa ? Px))).
 510
 511 notation > "'RAA' [ident H] term 90 b" with precedence 19
 512 for @{ 'Raa (λ${ident H}.show $b ?) }.
 513 interpretation "RAA KO" 'Raa p = (cast ? unit (Raa ? (cast ? (unit_to ?) p))).
 514 interpretation "RAA OK" 'Raa p = (Raa ? p).
 515
 516 (* ∃ introduction *)
 517 notation < "\infrule hbox(\emsp Pn \emsp) Px mstyle color #ff0000 (∃\sub\i)" with precedence 19
 518 for @{ 'Exists_intro_ko_1 $Pn $Px }.
 519 interpretation "Exists_intro_ko_1" 'Exists_intro_ko_1 Pn Px =
 520   (show Px (cast ? ? (Exists_intro ? ? ? (cast ? ? Pn)))).
 521
 522 notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) mstyle color #ff0000 (∃\sub\i)" with precedence 19
 523 for @{ 'Exists_intro_ko_2 $Pn $Px }.
 524 interpretation "Exists_intro_ko_2" 'Exists_intro_ko_2 Pn Px =
 525   (cast ? ? (show Px (cast ? ? (Exists_intro ? ? ? (cast ? ? Pn))))).
 526
 527 notation < "maction (\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)) (\vdots)" with precedence 19
 528 for @{ 'Exists_intro_ok_1 $Pn $Px }.
 529 interpretation "Exists_intro_ok_1" 'Exists_intro_ok_1 Pn Px =
 530   (show Px (Exists_intro ? ? ? Pn)).
 531
 532 notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) (∃\sub\i)" with precedence 19
 533 for @{ 'Exists_intro_ok_2 $Pn $Px }.
 534 interpretation "Exists_intro_ok_2" 'Exists_intro_ok_2 Pn Px =
 535   (cast ? ? (show Px (Exists_intro ? ? ? Pn))).
 536
 537 notation >"∃#'i' {term 90 t} term 90 Pt" non associative with precedence 19
 538 for @{'Exists_intro $t (λw.? w) (show $Pt ?)}.
 539 interpretation "Exists_intro KO" 'Exists_intro t P Pt =
 540  (cast ? ? (Exists_intro sort P t (cast ? ? Pt))).
 541 interpretation "Exists_intro OK" 'Exists_intro t P Pt =
 542  (Exists_intro sort P t Pt).
 543
 544 (* ∃ elimination *)
 545 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
 546 for @{ 'Exists_elim_ko_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 547 interpretation "Exists_elim_ko_1" 'Exists_elim_ko_1 ExPx Pc c =
 548     (show c (cast ? ? (Exists_elim ? ? ? (cast ? ? ExPx) (cast ? ? Pc)))).
 549
 550 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
 551 for @{ 'Exists_elim_ko_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 552 interpretation "Exists_elim_ko_2" 'Exists_elim_ko_2 ExPx Pc c =
 553     (cast ? ? (show c (cast ? ? (Exists_elim ? ? ? (cast ? ? ExPx) (cast ? ? Pc))))).
 554
 555 notation < "maction (\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)) (\vdots)" with precedence 19
 556 for @{ 'Exists_elim_ok_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 557 interpretation "Exists_elim_ok_1" 'Exists_elim_ok_1 ExPx Pc c =
 558     (show c (Exists_elim ? ? ? ExPx Pc)).
 559
 560 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
 561 for @{ 'Exists_elim_ok_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 562 interpretation "Exists_elim_ok_2" 'Exists_elim_ok_2 ExPx Pc c =
 563     (cast ? ? (show c (Exists_elim ? ? ? ExPx Pc))).
 564
 565 definition ex_concl := λx:sort → CProp.∀y:sort.unit → x y.
 566 definition ex_concl_dummy := ∀y:sort.unit → unit.
 567 definition fake_pred := λx:sort.unit.
 568
 569 notation >"∃#'e' term 90 ExPt {ident t} [ident H] term 90 c" non associative with precedence 19
 570 for @{'Exists_elim (λx.? x) (show $ExPt ?) (λ${ident t}:sort.λ${ident H}.show $c ?)}.
 571 interpretation "Exists_elim KO" 'Exists_elim P ExPt c =
 572  (cast ? ? (Exists_elim sort P ?
 573    (cast (Exists ? P)  ? ExPt)
 574    (cast ex_concl_dummy (ex_concl ?) c))).
 575 interpretation "Exists_elim OK" 'Exists_elim P ExPt c =
 576  (Exists_elim sort P ? ExPt c).
 577
 578 (* ∀ introduction *)
 579
 580 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19
 581 for @{ 'Forall_intro_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
 582 interpretation "Forall_intro_ko_1" 'Forall_intro_ko_1 Px Pn =
 583   (show Pn (cast ? ? (Forall_intro ? ? (cast ? ? Px)))).
 584
 585 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19
 586 for @{ 'Forall_intro_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
 587 interpretation "Forall_intro_ko_2" 'Forall_intro_ko_2 Px Pn =
 588   (cast ? ? (show Pn (cast ? ? (Forall_intro ? ? (cast ? ? Px))))).
 589
 590 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)) (\vdots)" with precedence 19
 591 for @{ 'Forall_intro_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
 592 interpretation "Forall_intro_ok_1" 'Forall_intro_ok_1 Px Pn =
 593   (show Pn (Forall_intro ? ? Px)).
 594
 595 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\i \emsp ident x)" with precedence 19
 596 for @{ 'Forall_intro_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
 597 interpretation "Forall_intro_ok_2" 'Forall_intro_ok_2 Px Pn =
 598   (cast ? ? (show Pn (Forall_intro ? ? Px))).
 599
 600 notation > "∀#'i' {ident y} term 90 Px" non associative with precedence 19
 601 for @{ 'Forall_intro (λ_.?) (λ${ident y}.show $Px ?) }.
 602 interpretation "Forall_intro KO" 'Forall_intro P Px =
 603   (cast ? ? (Forall_intro sort P (cast ? ? Px))).
 604 interpretation "Forall_intro OK" 'Forall_intro P Px =
 605   (Forall_intro sort P Px).
 606
 607 (* ∀ elimination *)
 608 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\e))" with precedence 19
 609 for @{ 'Forall_elim_ko_1 $Px $Pn }.
 610 interpretation "Forall_elim_ko_1" 'Forall_elim_ko_1 Px Pn =
 611   (show Pn (cast ? ? (Forall_elim ? ? ? (cast ? ? Px)))).
 612
 613 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\e))" with precedence 19
 614 for @{ 'Forall_elim_ko_2 $Px $Pn }.
 615 interpretation "Forall_elim_ko_2" 'Forall_elim_ko_2 Px Pn =
 616   (cast ? ? (show Pn (cast ? ? (Forall_elim ? ? ? (cast ? ? Px))))).
 617
 618 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\e)) (\vdots)" with precedence 19
 619 for @{ 'Forall_elim_ok_1 $Px $Pn }.
 620 interpretation "Forall_elim_ok_1" 'Forall_elim_ok_1 Px Pn =
 621   (show Pn (Forall_elim ? ? ? Px)).
 622
 623 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\e)" with precedence 19
 624 for @{ 'Forall_elim_ok_2 $Px $Pn }.
 625 interpretation "Forall_elim_ok_2" 'Forall_elim_ok_2 Px Pn =
 626   (cast ? ? (show Pn (Forall_elim ? ? ? Px))).
 627
 628 notation > "∀#'e' {term 90 t} term 90 Pn" non associative with precedence 19
 629 for @{ 'Forall_elim (λ_.?) $t (show $Pn ?) }.
 630 interpretation "Forall_elim KO" 'Forall_elim P t Px =
 631   (cast ? unit (Forall_elim sort P t (cast ? ? Px))).
 632 interpretation "Forall_elim OK" 'Forall_elim P t Px =
 633   (Forall_elim sort P t Px).
 634
 635 (* already proved lemma *)
 636 definition hide_args : ∀A:Type.A→A := λA:Type.λa:A.a.
 637 notation < "t" non associative with precedence 90 for @{'hide_args $t}.
 638 interpretation "hide 0 args"  'hide_args t = (hide_args ? t).
 639 interpretation "hide 1 args"  'hide_args t = (hide_args ? t ?).
 640 interpretation "hide 2 args"  'hide_args t = (hide_args ? t ? ?).
 641 interpretation "hide 3 args"  'hide_args t = (hide_args ? t ? ? ?).
 642 interpretation "hide 4 args"  'hide_args t = (hide_args ? t ? ? ? ?).
 643 interpretation "hide 5 args"  'hide_args t = (hide_args ? t ? ? ? ? ?).
 644 interpretation "hide 6 args"  'hide_args t = (hide_args ? t ? ? ? ? ? ?).
 645 interpretation "hide 7 args"  'hide_args t = (hide_args ? t ? ? ? ? ? ? ?).
 646
 647 (* more args crashes the pattern matcher *)
 648
 649 (* already proved lemma, 0 assumptions *)
 650 definition Lemma : ΠA.A→A ≝ λA:CProp.λa:A.a.
 651
 652 notation < "\infrule
 653          (\infrule
 654              (\emsp)
 655              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
 656          p \nbsp"
 657 non associative with precedence 19
 658 for @{ 'lemma_ko_1 $p ($H : $_) }.
 659 interpretation "lemma_ko_1" 'lemma_ko_1 p H =
 660   (show p (cast ? ? (Lemma ? (cast ? ? H)))).
 661
 662 notation < "\infrule
 663          (\infrule
 664              (\emsp)
 665              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
 666          mstyle color #ff0000 (p) \nbsp"
 667 non associative with precedence 19
 668 for @{ 'lemma_ko_2 $p ($H : $_) }.
 669 interpretation "lemma_ko_2" 'lemma_ko_2 p H =
 670   (cast ? ? (show p (cast ? ?
 671     (Lemma ? (cast ? ? H))))).
 672
 673
 674 notation < "\infrule
 675          (\infrule
 676              (\emsp)
 677              (╲ mstyle mathsize normal (H) ╱) \nbsp)
 678          p \nbsp"
 679 non associative with precedence 19
 680 for @{ 'lemma_ok_1 $p ($H : $_) }.
 681 interpretation "lemma_ok_1" 'lemma_ok_1 p H =
 682   (show p (Lemma ? H)).
 683
 684 notation < "\infrule
 685          (\infrule
 686              (\emsp)
 687              (╲ mstyle mathsize normal (H) ╱) \nbsp)
 688          mstyle color #ff0000 (p) \nbsp"
 689 non associative with precedence 19
 690 for @{ 'lemma_ok_2 $p ($H : $_) }.
 691 interpretation "lemma_ok_2" 'lemma_ok_2 p H =
 692   (cast ? ? (show p (Lemma ? H))).
 693
 694 notation > "'lem' 0 term 90 l" non associative with precedence 19
 695 for @{ 'Lemma (hide_args ? $l : ?) }.
 696 interpretation "lemma KO" 'Lemma l =
 697   (cast ? ? (Lemma unit (cast unit ? l))).
 698 interpretation "lemma OK" 'Lemma l = (Lemma ? l).
 699
 700
 701 (* already proved lemma, 1 assumption *)
 702 definition Lemma1 : ΠA,B. (A ⇒ B) → A → B ≝
 703  λA,B:CProp.λf:A⇒B.λa:A.
 704   Imply_elim A B f a.
 705
 706 notation < "\infrule
 707          (\infrule
 708              (\emsp a \emsp)
 709              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
 710          p \nbsp"
 711 non associative with precedence 19
 712 for @{ 'lemma1_ko_1 $a $p ($H : $_) }.
 713 interpretation "lemma1_ko_1" 'lemma1_ko_1 a p H =
 714   (show p (cast ? ? (Lemma1 ? ? (cast ? ? H) (cast ? ? a)))).
 715
 716 notation < "\infrule
 717          (\infrule
 718              (\emsp a \emsp)
 719              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
 720          mstyle color #ff0000 (p) \nbsp"
 721 non associative with precedence 19
 722 for @{ 'lemma1_ko_2 $a $p ($H : $_) }.
 723 interpretation "lemma1_ko_2" 'lemma1_ko_2 a p H =
 724   (cast ? ? (show p (cast ? ?
 725     (Lemma1 ? ? (cast ? ? H) (cast ? ? a))))).
 726
 727
 728 notation < "\infrule
 729          (\infrule
 730              (\emsp a \emsp)
 731              (╲ mstyle mathsize normal (H) ╱) \nbsp)
 732          p \nbsp"
 733 non associative with precedence 19
 734 for @{ 'lemma1_ok_1 $a $p ($H : $_) }.
 735 interpretation "lemma1_ok_1" 'lemma1_ok_1 a p H =
 736   (show p (Lemma1 ? ? H a)).
 737
 738 notation < "\infrule
 739          (\infrule
 740              (\emsp a \emsp)
 741              (╲ mstyle mathsize normal (H) ╱) \nbsp)
 742          mstyle color #ff0000 (p) \nbsp"
 743 non associative with precedence 19
 744 for @{ 'lemma1_ok_2 $a $p ($H : $_) }.
 745 interpretation "lemma1_ok_2" 'lemma1_ok_2 a p H =
 746   (cast ? ? (show p (Lemma1 ? ? H a))).
 747
 748
 749 notation > "'lem' 1 term 90 l term 90 p" non associative with precedence 19
 750 for @{ 'Lemma1 (hide_args ? $l : ?) (show $p ?) }.
 751 interpretation "lemma 1 KO" 'Lemma1 l p =
 752   (cast ? ? (Lemma1 unit unit (cast (Imply unit unit) ? l) (cast unit ? p))).
 753 interpretation "lemma 1 OK" 'Lemma1 l p = (Lemma1 ? ? l p).
 754
 755 (* already proved lemma, 2 assumptions *)
 756 definition Lemma2 : ΠA,B,C. (A ⇒ B ⇒ C) → A → B → C ≝
 757  λA,B,C:CProp.λf:A⇒B⇒C.λa:A.λb:B.
 758   Imply_elim B C (Imply_elim A (B⇒C) f a) b.
 759
 760 notation < "\infrule
 761          (\infrule
 762              (\emsp a \emsp\emsp\emsp b \emsp)
 763              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
 764          p \nbsp"
 765 non associative with precedence 19
 766 for @{ 'lemma2_ko_1 $a $b $p ($H : $_) }.
 767 interpretation "lemma2_ko_1" 'lemma2_ko_1 a b p H =
 768   (show p (cast ? ? (Lemma2 ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b)))).
 769
 770 notation < "\infrule
 771          (\infrule
 772              (\emsp a \emsp\emsp\emsp b \emsp)
 773              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
 774          mstyle color #ff0000 (p) \nbsp"
 775 non associative with precedence 19
 776 for @{ 'lemma2_ko_2 $a $b $p ($H : $_) }.
 777 interpretation "lemma2_ko_2" 'lemma2_ko_2 a b p H =
 778   (cast ? ? (show p (cast ? ?
 779     (Lemma2 ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b))))).
 780
 781
 782 notation < "\infrule
 783          (\infrule
 784              (\emsp a \emsp\emsp\emsp b \emsp)
 785              (╲ mstyle mathsize normal (H) ╱) \nbsp)
 786          p \nbsp"
 787 non associative with precedence 19
 788 for @{ 'lemma2_ok_1 $a $b $p ($H : $_) }.
 789 interpretation "lemma2_ok_1" 'lemma2_ok_1 a b p H =
 790   (show p (Lemma2 ? ? ? H a b)).
 791
 792 notation < "\infrule
 793          (\infrule
 794              (\emsp a \emsp\emsp\emsp b \emsp)
 795              (╲ mstyle mathsize normal (H) ╱) \nbsp)
 796          mstyle color #ff0000 (p) \nbsp"
 797 non associative with precedence 19
 798 for @{ 'lemma2_ok_2 $a $b $p ($H : $_) }.
 799 interpretation "lemma2_ok_2" 'lemma2_ok_2 a b p H =
 800   (cast ? ? (show p (Lemma2 ? ? ? H a b))).
 801
 802 notation > "'lem' 2 term 90 l term 90 p term 90 q" non associative with precedence 19
 803 for @{ 'Lemma2 (hide_args ? $l : ?) (show $p ?) (show $q ?) }.
 804 interpretation "lemma 2 KO" 'Lemma2 l p q =
 805   (cast ? ? (Lemma2 unit unit unit (cast (Imply unit (Imply unit unit)) ? l) (cast unit ? p) (cast unit ? q))).
 806 interpretation "lemma 2 OK" 'Lemma2 l p q = (Lemma2 ? ? ? l p q).
 807
 808 (* already proved lemma, 3 assumptions *)
 809 definition Lemma3 : ΠA,B,C,D. (A ⇒ B ⇒ C ⇒ D) → A → B → C → D ≝
 810  λA,B,C,D:CProp.λf:A⇒B⇒C⇒D.λa:A.λb:B.λc:C.
 811   Imply_elim C D (Imply_elim B (C⇒D) (Imply_elim A (B⇒C⇒D) f a) b) c.
 812
 813 notation < "\infrule
 814          (\infrule
 815              (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
 816              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
 817          p \nbsp"
 818 non associative with precedence 19
 819 for @{ 'lemma3_ko_1 $a $b $c $p ($H : $_) }.
 820 interpretation "lemma3_ko_1" 'lemma3_ko_1 a b c p H =
 821   (show p (cast ? ?
 822    (Lemma3 ? ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b) (cast ? ? c)))).
 823
 824 notation < "\infrule
 825          (\infrule
 826              (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
 827              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
 828          mstyle color #ff0000 (p) \nbsp"
 829 non associative with precedence 19
 830 for @{ 'lemma3_ko_2 $a $b $c $p ($H : $_) }.
 831 interpretation "lemma3_ko_2" 'lemma3_ko_2 a b c p H =
 832   (cast ? ? (show p (cast ? ?
 833     (Lemma3 ? ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b) (cast ? ? c))))).
 834
 835
 836 notation < "\infrule
 837          (\infrule
 838              (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
 839              (╲ mstyle mathsize normal (H) ╱) \nbsp)
 840          p \nbsp"
 841 non associative with precedence 19
 842 for @{ 'lemma3_ok_1 $a $b $c $p ($H : $_) }.
 843 interpretation "lemma3_ok_1" 'lemma3_ok_1 a b c p H =
 844   (show p (Lemma3 ? ? ? ? H a b c)).
 845
 846 notation < "\infrule
 847          (\infrule
 848              (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
 849              (╲ mstyle mathsize normal (H) ╱) \nbsp)
 850          mstyle color #ff0000 (p) \nbsp"
 851 non associative with precedence 19
 852 for @{ 'lemma3_ok_2 $a $b $c $p ($H : $_) }.
 853 interpretation "lemma3_ok_2" 'lemma3_ok_2 a b c p H =
 854   (cast ? ? (show p (Lemma3 ? ? ? ? H a b c))).
 855
 856 notation > "'lem' 3 term 90 l term 90 p term 90 q term 90 r" non associative with precedence 19
 857 for @{ 'Lemma3 (hide_args ? $l : ?) (show $p ?) (show $q ?) (show $r ?) }.
 858 interpretation "lemma 3 KO" 'Lemma3 l p q r =
 859   (cast ? ? (Lemma3 unit unit unit unit (cast (Imply unit (Imply unit (Imply unit unit))) ? l) (cast unit ? p) (cast unit ? q) (cast unit ? r))).
 860 interpretation "lemma 3 OK" 'Lemma3 l p q r = (Lemma3 ? ? ? ? l p q r).