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 assumpt := λA:CProp.λa:A.
  44   a.
  45
  46 axiom Raa : ∀A.(Not A → Bot) → A.
  47
  48 (* Dummy proposition *)
  49 axiom unit : CProp.
  50
  51 (* Notations *)
  52 notation "hbox(a break ⇒ b)" right associative with precedence 20
  53 for @{ 'Imply $a $b }.
  54 interpretation "Imply" 'Imply a b = (Imply a b).
  55 interpretation "constructive or" 'or x y = (Or x y).
  56 interpretation "constructive and" 'and x y = (And x y).
  57 notation "⊤" non associative with precedence 90 for @{'Top}.
  58 interpretation "Top" 'Top = Top.
  59 notation "⊥" non associative with precedence 90 for @{'Bot}.
  60 interpretation "Bot" 'Bot = Bot.
  61 interpretation "Not" 'not a = (Not a).
  62 notation "✶" non associative with precedence 90 for @{'unit}.
  63 interpretation "dummy prop" 'unit = unit.
  64
  65 (* Variables *)
  66 axiom A : CProp.
  67 axiom B : CProp.
  68 axiom C : CProp.
  69 axiom D : CProp.
  70 axiom E : CProp.
  71 axiom F : CProp.
  72 axiom G : CProp.
  73 axiom H : CProp.
  74 axiom I : CProp.
  75 axiom J : CProp.
  76 axiom K : CProp.
  77 axiom L : CProp.
  78 axiom M : CProp.
  79 axiom N : CProp.
  80 axiom O : CProp.
  81 axiom P : CProp.
  82 axiom Q : CProp.
  83 axiom R : CProp.
  84 axiom S : CProp.
  85 axiom T : CProp.
  86 axiom U : CProp.
  87 axiom V : CProp.
  88 axiom W : CProp.
  89 axiom X : CProp.
  90 axiom Y : CProp.
  91 axiom Z : CProp.
  92
  93 (* Every formula user provided annotates its proof A becomes (show A ?) *)
  94 definition show : ∀A.A→A ≝ λA:CProp.λa:A.a.
  95
  96 (* When something does not fit, this daemon is used *)
  97 axiom cast: ∀A,B:CProp.B → A.
  98
  99
 100 notation > "'prove' p" non associative with precedence 19
 101 for @{ 'prove $p }.
 102 interpretation "prove KO" 'prove p = (cast _ _ (show p _)).
 103 interpretation "prove OK" 'prove p = (show p _).
 104
 105 notation < "\infrule (t\atop ⋮) a ?" with precedence 19 for @{ 'leaf_ok $a $t }.
 106 interpretation "leaf OK" 'leaf_ok a t = (show a t).
 107 notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19 for @{ 'leaf_ko $a $t }.
 108 interpretation "leaf KO" 'leaf_ko a t = (cast _ a (show _ t)).
 109
 110 notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 for @{ 'assumpt_ko $a $H }.
 111 interpretation "assumption_ko 1" 'assumpt_ko a H = (show a (cast _ _ (assumpt _ H))).
 112 interpretation "assumption_ko 2" 'assumpt_ko a H = (cast _ _ (show a (cast _ _ (assumpt _ H)))).
 113
 114 notation < "[ a ] \sup H" with precedence 19 for @{ 'assumpt_ok $a $H }.
 115 interpretation "assumption_ok 1" 'assumpt_ok a H = (show a (assumpt a H)).
 116 notation < "[ mstyle color #ff0000 (a) ] \sup H" with precedence 19 for @{ 'assumpt_ok_2 $a $H }.
 117 interpretation "assumption_ok 2" 'assumpt_ok_2 a H = (cast _ _ (show a (assumpt a H))).
 118
 119 notation > "[H]" with precedence 90 for @{ 'assumpt $H }.
 120 interpretation "assumpt KO" 'assumpt H = (cast _ _ (assumpt _ H)).
 121 interpretation "assumpt OK" 'assumpt H = (assumpt _ H).
 122
 123 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
 124 for @{ 'Imply_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
 125 interpretation "Imply_intro_ko_1" 'Imply_intro_ko_1 ab \eta.b =
 126   (show ab (cast _ _ (Imply_intro _ _ b))).
 127
 128 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
 129 for @{ 'Imply_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
 130 interpretation "Imply_intro_ko_1" 'Imply_intro_ko_2 ab \eta.b =
 131   (cast _ _ (show ab (cast _ _ (Imply_intro _ _ b)))).
 132
 133 notation < "\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) " with precedence 19
 134 for @{ 'Imply_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
 135 interpretation "Imply_intro_ok_1" 'Imply_intro_ok_1 ab \eta.b =
 136   (show ab (Imply_intro _ _ b)).
 137
 138 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (⇒\sub\i \emsp ident H) " with precedence 19
 139 for @{ 'Imply_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
 140 interpretation "Imply_intro_ok_2" 'Imply_intro_ok_2 ab \eta.b =
 141   (cast _ _ (show ab (Imply_intro _ _ b))).
 142
 143 notation > "⇒_'i' [ident H] term 90 b" with precedence 19
 144 for @{ 'Imply_intro $b (λ${ident H}.show $b ?) }.
 145 interpretation "Imply_intro KO" 'Imply_intro b pb = (cast _ (Imply unit b) (Imply_intro _ b pb)).
 146 interpretation "Imply_intro OK" 'Imply_intro b pb = (Imply_intro _ b pb).
 147
 148 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19 for @{ 'Imply_elim_ko_1 $ab $a $b }.
 149 interpretation "Imply_elim_ko_1" 'Imply_elim_ko_1 ab a b =
 150   (show b (cast _ _ (Imply_elim _ _ ab a))).
 151 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19 for @{ 'Imply_elim_ko_2 $ab $a $b }.
 152 interpretation "Imply_elim_ko_2" 'Imply_elim_ko_2 ab a b =
 153   (cast _ _ (show b (cast _ _ (Imply_elim _ _ ab a)))).
 154
 155 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) " with precedence 19
 156 for @{ 'Imply_elim_ok_1 $ab $a $b }.
 157 interpretation "Imply_elim_ok_1" 'Imply_elim_ok_1 ab a b =
 158   (show b (Imply_elim _ _ ab a)).
 159
 160 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (⇒\sub\e) " with precedence 19
 161 for @{ 'Imply_elim_ok_2 $ab $a $b }.
 162 interpretation "Imply_elim_ok_2" 'Imply_elim_ok_2 ab a b =
 163   (cast _ _ (show b (Imply_elim _ _ ab a))).
 164
 165 notation > "⇒_'e' term 90 ab term 90 a" with precedence 19 for @{ 'Imply_elim (show $ab ?) (show $a ?) }.
 166 interpretation "Imply_elim KO" 'Imply_elim ab a = (cast _ _ (Imply_elim _ _ (cast (Imply unit unit) _ ab) (cast unit _ a))).
 167 interpretation "Imply_elim OK" 'Imply_elim ab a = (Imply_elim _ _ ab a).
 168
 169 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19 for @{ 'And_intro_ko_1 $a $b $ab }.
 170 interpretation "And_intro_ko_1" 'And_intro_ko_1 a b ab =
 171   (show ab (cast _ _ (And_intro _ _ a b))).
 172 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19 for @{ 'And_intro_ko_2 $a $b $ab }.
 173 interpretation "And_intro_ko_2" 'And_intro_ko_2 a b ab =
 174   (cast _ _ (show ab (cast _ _ (And_intro _ _ a b)))).
 175
 176 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)" with precedence 19
 177 for @{ 'And_intro_ok_1 $a $b $ab }.
 178 interpretation "And_intro_ok_1" 'And_intro_ok_1 a b ab =
 179   (show ab (And_intro _ _ a b)).
 180
 181 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) (∧\sub\i)" with precedence 19
 182 for @{ 'And_intro_ok_2 $a $b $ab }.
 183 interpretation "And_intro_ok_2" 'And_intro_ok_2 a b ab =
 184   (cast _ _ (show ab (And_intro _ _ a b))).
 185
 186 notation > "∧_'i' term 90 a term 90 b" with precedence 19 for @{ 'And_intro (show $a ?) (show $b ?) }.
 187 interpretation "And_intro KO" 'And_intro a b = (cast _ _ (And_intro _ _ a b)).
 188 interpretation "And_intro OK" 'And_intro a b = (And_intro _ _ a b).
 189
 190 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19
 191 for @{ 'And_elim_l_ko_1 $ab $a }.
 192 interpretation "And_elim_l_ko_1" 'And_elim_l_ko_1 ab a =
 193   (show a (cast _ _ (And_elim_l _ _ ab))).
 194
 195 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19
 196 for @{ 'And_elim_l_ko_2 $ab $a }.
 197 interpretation "And_elim_l_ko_2" 'And_elim_l_ko_2 ab a =
 198   (cast _ _ (show a (cast _ _ (And_elim_l _ _ ab)))).
 199
 200 notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))" with precedence 19
 201 for @{ 'And_elim_l_ok_1 $ab $a }.
 202 interpretation "And_elim_l_ok_1" 'And_elim_l_ok_1 ab a =
 203   (show a (And_elim_l _ _ ab)).
 204
 205 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\l))" with precedence 19
 206 for @{ 'And_elim_l_ok_2 $ab $a }.
 207 interpretation "And_elim_l_ok_2" 'And_elim_l_ok_2 ab a =
 208   (cast _ _ (show a (And_elim_l _ _ ab))).
 209
 210 notation > "∧_'e_l' term 90 ab" with precedence 19
 211 for @{ 'And_elim_l (show $ab ?) }.
 212 interpretation "And_elim_l KO" 'And_elim_l a = (And_elim_l _ _ (cast (And _ unit) _ a)).
 213 interpretation "And_elim_l OK" 'And_elim_l a = (And_elim_l _ _ a).
 214
 215 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19
 216 for @{ 'And_elim_r_ko_1 $ab $a }.
 217 interpretation "And_elim_r_ko_1" 'And_elim_r_ko_1 ab a =
 218   (show a (cast _ _ (And_elim_r _ _ ab))).
 219
 220 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19
 221 for @{ 'And_elim_r_ko_2 $ab $a }.
 222 interpretation "And_elim_r_ko_2" 'And_elim_r_ko_2 ab a =
 223   (cast _ _ (show a (cast _ _ (And_elim_r _ _ ab)))).
 224
 225 notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))" with precedence 19
 226 for @{ 'And_elim_r_ok_1 $ab $a }.
 227 interpretation "And_elim_r_ok_1" 'And_elim_r_ok_1 ab a =
 228   (show a (And_elim_r _ _ ab)).
 229
 230 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\r))" with precedence 19
 231 for @{ 'And_elim_r_ok_2 $ab $a }.
 232 interpretation "And_elim_r_ok_2" 'And_elim_r_ok_2 ab a =
 233   (cast _ _ (show a (And_elim_r _ _ ab))).
 234
 235 notation > "∧_'e_r' term 90 ab" with precedence 19
 236 for @{ 'And_elim_r (show $ab ?) }.
 237 interpretation "And_elim_r KO" 'And_elim_r a = (And_elim_r _ _ (cast (And unit _) _ a)).
 238 interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r _ _ a).
 239
 240 notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))" with precedence 19
 241 for @{ 'Or_intro_l_ok_1 $a $ab }.
 242 interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab =
 243   (show ab (Or_intro_l _ _ a)).
 244
 245 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19
 246 for @{ 'Or_intro_l_ok_1 $a $ab }.
 247 interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab =
 248   (cast _ _ (show ab (Or_intro_l _ _ a))).
 249
 250 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19
 251 for @{ 'Or_intro_l_ko_1 $a $ab }.
 252 interpretation "Or_intro_l_ko_1" 'Or_intro_l_ko_1 a ab =
 253   (show ab (cast _ _ (Or_intro_l _ _ a))).
 254
 255 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19
 256 for @{ 'Or_intro_l_ko_2 $a $ab }.
 257 interpretation "Or_intro_l_ko_2" 'Or_intro_l_ko_2 a ab =
 258   (cast _ _ (show ab (cast _ _ (Or_intro_l _ _ a)))).
 259
 260 notation > "∨_'i_l' term 90 a" with precedence 19
 261 for @{ 'Or_intro_l (show $a ?) }.
 262 interpretation "Or_intro_l KO" 'Or_intro_l a = (cast _ (Or _ unit) (Or_intro_l _ _ a)).
 263 interpretation "Or_intro_l OK" 'Or_intro_l a = (Or_intro_l _ _ a).
 264
 265 notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))" with precedence 19
 266 for @{ 'Or_intro_r_ok_1 $a $ab }.
 267 interpretation "Or_intro_r_ok_1" 'Or_intro_r_ok_1 a ab =
 268   (show ab (Or_intro_r _ _ a)).
 269
 270 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\r))" with precedence 19
 271 for @{ 'Or_intro_r_ok_1 $a $ab }.
 272 interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab =
 273   (cast _ _ (show ab (Or_intro_r _ _ a))).
 274
 275 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19
 276 for @{ 'Or_intro_r_ko_1 $a $ab }.
 277 interpretation "Or_intro_r_ko_1" 'Or_intro_r_ko_1 a ab =
 278   (show ab (cast _ _ (Or_intro_r _ _ a))).
 279
 280 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19
 281 for @{ 'Or_intro_r_ko_2 $a $ab }.
 282 interpretation "Or_intro_r_ko_2" 'Or_intro_r_ko_2 a ab =
 283   (cast _ _ (show ab (cast _ _ (Or_intro_r _ _ a)))).
 284
 285 notation > "∨_'i_r' term 90 a" with precedence 19
 286 for @{ 'Or_intro_r (show $a ?) }.
 287 interpretation "Or_intro_r KO" 'Or_intro_r a = (cast _ (Or unit _) (Or_intro_r _ _ a)).
 288 interpretation "Or_intro_r OK" 'Or_intro_r a = (Or_intro_r _ _ a).
 289
 290 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
 291 for @{ 'Or_elim_ok_1 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 292 interpretation "Or_elim_ok_1" 'Or_elim_ok_1 ab \eta.ac \eta.bc c =
 293   (show c (Or_elim _ _ _ ab ac bc)).
 294
 295 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
 296 for @{ 'Or_elim_ok_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 297 interpretation "Or_elim_ok_2" 'Or_elim_ok_2 ab \eta.ac \eta.bc c =
 298   (cast _ _ (show c (Or_elim _ _ _ ab ac bc))).
 299
 300 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
 301 for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }.
 302 interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc =
 303   (show c (cast _ _ (Or_elim _ _ _ ab (cast _ _ ac) (cast _ _ bc)))).
 304
 305 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
 306 for @{ 'Or_elim_ko_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 307 interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c =
 308   (cast _ _ (show c (cast _ _ (Or_elim _ _ _ ab (cast _ _ ac) (cast _ _ bc))))).
 309
 310 definition unit_to ≝ λx:CProp.unit → x.
 311
 312 notation > "∨_'e' term 90 ab [ident Ha] term 90 cl [ident Hb] term 90 cr" with precedence 19
 313 for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) $cl $cr }.
 314 interpretation "Or_elim KO" 'Or_elim ab ac bc c1 c2 =
 315   (cast _ _ (Or_elim _ _ _ (cast (Or unit unit) _ ab) (cast (unit_to unit) (unit_to _) ac) (cast (unit_to unit) (unit_to _) bc))).
 316 interpretation "Or_elim OK" 'Or_elim ab ac bc c1 c2 = (Or_elim _ _ _ ab ac bc).
 317
 318 notation < "\infrule \nbsp ⊤ mstyle color #ff0000 (⊤\sub\i)" with precedence 19
 319 for @{'Top_intro_ko_1}.
 320 interpretation "Top_intro_ko_1" 'Top_intro_ko_1 = (show _ (cast _ _ Top_intro)).
 321
 322 notation < "\infrule \nbsp ⊤ (⊤\sub\i)" with precedence 19
 323 for @{'Top_intro_ok_1}.
 324 interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show _ Top_intro).
 325
 326 notation > "⊤_'i'" with precedence 19 for @{ 'Top_intro }.
 327 interpretation "Top_intro KO" 'Top_intro = (cast _ _ Top_intro).
 328 interpretation "Top_intro OK" 'Top_intro = Top_intro.
 329
 330 notation < "\infrule b a (⊥\sub\e)" with precedence 19 for @{'Bot_elim_ok_1 $a $b}.
 331 interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b =
 332   (show a (Bot_elim a b)).
 333
 334 notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19 for @{'Bot_elim_ko_1 $a $b}.
 335 interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b =
 336   (show a (Bot_elim a (cast _ _ b))).
 337
 338 notation > "⊥_'e' term 90 b" with precedence 19
 339 for @{ 'Bot_elim (show $b ?) }.
 340 interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim _ (cast _ _ a)).
 341 interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim _ a).
 342
 343 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub\i) \emsp ident H)" with precedence 19
 344 for @{ 'Not_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
 345 interpretation "Not_intro_ko_1" 'Not_intro_ko_1 ab \eta.b =
 346   (show ab (cast _ _ (Not_intro _ (cast _ _ b)))).
 347
 348 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub\i) \emsp ident H)" with precedence 19
 349 for @{ 'Not_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
 350 interpretation "Not_intro_ko_2" 'Not_intro_ko_2 ab \eta.b =
 351   (cast _ _ (show ab (cast _ _ (Not_intro _ (cast _ _ b))))).
 352
 353 notation < "\infrule hbox(\emsp b \emsp) ab (\lnot\sub\i \emsp ident H) " with precedence 19
 354 for @{ 'Not_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
 355 interpretation "Not_intro_ok_1" 'Not_intro_ok_1 ab \eta.b =
 356   (show ab (Not_intro _ b)).
 357
 358 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub\i \emsp ident H) " with precedence 19
 359 for @{ 'Not_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
 360 interpretation "Not_intro_ok_2" 'Not_intro_ok_2 ab \eta.b =
 361   (cast _ _ (show ab (Not_intro _ b))).
 362
 363 notation > "¬_'i' [ident H] term 90 b" with precedence 19
 364 for @{ 'Not_intro (λ${ident H}.show $b ?) }.
 365 interpretation "Not_intro KO" 'Not_intro a = (cast _ _ (Not_intro _ (cast _ _ a))).
 366 interpretation "Not_intro OK" 'Not_intro a = (Not_intro _ a).
 367
 368 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub\e) " with precedence 19
 369 for @{ 'Not_elim_ok_1 $ab $a $b }.
 370 interpretation "Not_elim_ok_1" 'Not_elim_ok_1 ab a b =
 371   (show b (Not_elim _ ab a)).
 372
 373 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (\lnot\sub\e) " with precedence 19
 374 for @{ 'Not_elim_ok_2 $ab $a $b }.
 375 interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b =
 376   (cast _ _ (show b (Not_elim _ ab a))).
 377
 378 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub\e) " with precedence 19
 379 for @{ 'Not_elim_ko_1 $ab $a $b }.
 380 interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b =
 381   (show b (Not_elim _ (cast _ _ ab) a)).
 382
 383 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub\e) " with precedence 19
 384 for @{ 'Not_elim_ko_2 $ab $a $b }.
 385 interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b =
 386   (cast _ _ (show b (Not_elim _ (cast _ _ ab) a))).
 387
 388 notation > "¬_'e' term 90 ab term 90 a" with precedence 19
 389 for @{ 'Not_elim (show $ab ?) (show $a ?) }.
 390 interpretation "Not_elim KO" 'Not_elim ab a = (Not_elim _ (cast _ _ ab) a).
 391 interpretation "Not_elim OK" 'Not_elim ab a = (Not_elim _ ab a).
 392
 393 notation < "\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)" with precedence 19
 394 for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
 395 interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn =
 396   (show Pn (Raa _ Px)).
 397
 398 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (\RAA \emsp ident x)" with precedence 19
 399 for @{ 'RAA_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
 400 interpretation "RAA_ok_2" 'RAA_ok_2 Px Pn =
 401   (cast _ _ (show Pn (Raa _ Px))).
 402
 403 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
 404 for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
 405 interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn =
 406   (show Pn (Raa _ (cast _ _ Px))).
 407
 408 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
 409 for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
 410 interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn =
 411   (cast _ _ (show Pn (Raa _ (cast _ _ Px)))).
 412
 413 notation > "'RAA' [ident H] term 90 b" with precedence 19
 414 for @{ 'Raa (λ${ident H}.show $b ?) }.
 415 interpretation "RAA KO" 'Raa p = (Raa _ (cast _ (unit_to _) p)).
 416 interpretation "RAA OK" 'Raa p = (Raa _ p).
 417
 418 (*DOCBEGIN
 419 Templates for rules
 420 ⇒_i […] (…)
 421 ∧_i (…) (…)
 422 ∨_i_l (…)
 423 ∨_i_r (…)
 424 ¬_i […] (…)
 425 ⊤_i
 426 ⇒_e (…) (…)
 427 ∧_e_l (…)
 428 ∧_e_r (…)
 429 ∨_e (…) […] (…) […] (…)
 430 ¬_e (…) (…)
 431 ⊥_e (…)
 432 prove (…)
 433 RAA […] (…)
 434 DOCEND*)
 435
 436
 437
 438