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

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