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