helm/software/matita/contribs/ng_assembly2/common/theory.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "common/pts.ma".
  24
  25 (* ********************************** *)
  26 (* SOTTOINSIEME MINIMALE DELLA TEORIA *)
  27 (* ********************************** *)
  28
  29 (* logic/connectives.ma *)
  30
  31 ninductive True: Prop ≝
  32  I : True.
  33
  34 ninductive False: Prop ≝.
  35
  36 ndefinition Not: Prop → Prop ≝
  37 λA.(A → False).
  38
  39 interpretation "logical not" 'not x = (Not x).
  40
  41 nlemma absurd : ∀A,C:Prop.A → ¬A → C.
  42  #A; #C; #H;
  43  nnormalize;
  44  #H1;
  45  nelim (H1 H).
  46 nqed.
  47
  48 nlemma not_to_not : ∀A,B:Prop. (A → B) → ((¬B) → (¬A)).
  49  #A; #B; #H;
  50  nnormalize;
  51  #H1; #H2;
  52  nelim (H1 (H H2)).
  53 nqed.
  54
  55 nlemma prop_to_nnprop : ∀P.P → ¬¬P.
  56  #P; nnormalize; #H; #H1;
  57  napply (H1 H).
  58 nqed.
  59
  60 ninductive And2 (A,B:Prop) : Prop ≝
  61  conj2 : A → B → (And2 A B).
  62
  63 interpretation "logical and" 'and x y = (And2 x y).
  64
  65 nlemma proj2_1: ∀A,B:Prop.A ∧ B → A.
  66  #A; #B; #H;
  67  napply (And2_ind A B … H);
  68  #H1; #H2;
  69  napply H1.
  70 nqed.
  71
  72 nlemma proj2_2: ∀A,B:Prop.A ∧ B → B.
  73  #A; #B; #H;
  74  napply (And2_ind A B … H);
  75  #H1; #H2;
  76  napply H2.
  77 nqed.
  78
  79 ninductive And3 (A,B,C:Prop) : Prop ≝
  80  conj3 : A → B → C → (And3 A B C).
  81
  82 nlemma proj3_1: ∀A,B,C:Prop.And3 A B C → A.
  83  #A; #B; #C; #H;
  84  napply (And3_ind A B C … H);
  85  #H1; #H2; #H3;
  86  napply H1.
  87 nqed.
  88
  89 nlemma proj3_2: ∀A,B,C:Prop.And3 A B C → B.
  90  #A; #B; #C; #H;
  91  napply (And3_ind A B C … H);
  92  #H1; #H2; #H3;
  93  napply H2.
  94 nqed.
  95
  96 nlemma proj3_3: ∀A,B,C:Prop.And3 A B C → C.
  97  #A; #B; #C; #H;
  98  napply (And3_ind A B C … H);
  99  #H1; #H2; #H3;
 100  napply H3.
 101 nqed.
 102
 103 ninductive And4 (A,B,C,D:Prop) : Prop ≝
 104  conj4 : A → B → C → D → (And4 A B C D).
 105
 106 nlemma proj4_1: ∀A,B,C,D:Prop.And4 A B C D → A.
 107  #A; #B; #C; #D; #H;
 108  napply (And4_ind A B C D … H);
 109  #H1; #H2; #H3; #H4;
 110  napply H1.
 111 nqed.
 112
 113 nlemma proj4_2: ∀A,B,C,D:Prop.And4 A B C D → B.
 114  #A; #B; #C; #D; #H;
 115  napply (And4_ind A B C D … H);
 116  #H1; #H2; #H3; #H4;
 117  napply H2.
 118 nqed.
 119
 120 nlemma proj4_3: ∀A,B,C,D:Prop.And4 A B C D → C.
 121  #A; #B; #C; #D; #H;
 122  napply (And4_ind A B C D … H);
 123  #H1; #H2; #H3; #H4;
 124  napply H3.
 125 nqed.
 126
 127 nlemma proj4_4: ∀A,B,C,D:Prop.And4 A B C D → D.
 128  #A; #B; #C; #D; #H;
 129  napply (And4_ind A B C D … H);
 130  #H1; #H2; #H3; #H4;
 131  napply H4.
 132 nqed.
 133
 134 ninductive And5 (A,B,C,D,E:Prop) : Prop ≝
 135  conj5 : A → B → C → D → E → (And5 A B C D E).
 136
 137 nlemma proj5_1: ∀A,B,C,D,E:Prop.And5 A B C D E → A.
 138  #A; #B; #C; #D; #E; #H;
 139  napply (And5_ind A B C D E … H);
 140  #H1; #H2; #H3; #H4; #H5;
 141  napply H1.
 142 nqed.
 143
 144 nlemma proj5_2: ∀A,B,C,D,E:Prop.And5 A B C D E → B.
 145  #A; #B; #C; #D; #E; #H;
 146  napply (And5_ind A B C D E … H);
 147  #H1; #H2; #H3; #H4; #H5;
 148  napply H2.
 149 nqed.
 150
 151 nlemma proj5_3: ∀A,B,C,D,E:Prop.And5 A B C D E → C.
 152  #A; #B; #C; #D; #E; #H;
 153  napply (And5_ind A B C D E … H);
 154  #H1; #H2; #H3; #H4; #H5;
 155  napply H3.
 156 nqed.
 157
 158 nlemma proj5_4: ∀A,B,C,D,E:Prop.And5 A B C D E → D.
 159  #A; #B; #C; #D; #E; #H;
 160  napply (And5_ind A B C D E … H);
 161  #H1; #H2; #H3; #H4; #H5;
 162  napply H4.
 163 nqed.
 164
 165 nlemma proj5_5: ∀A,B,C,D,E:Prop.And5 A B C D E → E.
 166  #A; #B; #C; #D; #E; #H;
 167  napply (And5_ind A B C D E … H);
 168  #H1; #H2; #H3; #H4; #H5;
 169  napply H5.
 170 nqed.
 171
 172 ninductive Or2 (A,B:Prop) : Prop ≝
 173   or2_intro1 : A → (Or2 A B)
 174 | or2_intro2 : B → (Or2 A B).
 175
 176 interpretation "logical or" 'or x y = (Or2 x y).
 177
 178 ndefinition decidable ≝ λA:Prop.A ∨ (¬A).
 179
 180 nlemma or2_elim
 181  : ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q.
 182  #P1; #P2; #Q; #H; #f1; #f2;
 183  napply (Or2_ind P1 P2 ? f1 f2 ?);
 184  napply H.
 185 nqed.
 186
 187 nlemma symmetric_or2 : ∀P1,P2.Or2 P1 P2 → Or2 P2 P1.
 188  #P1; #P2; #H;
 189  napply (or2_elim P1 P2 ? H);
 190  ##[ ##1: #H1; napply (or2_intro2 P2 P1 H1)
 191  ##| ##2: #H1; napply (or2_intro1 P2 P1 H1)
 192  ##]
 193 nqed.
 194
 195 ninductive Or3 (A,B,C:Prop) : Prop ≝
 196   or3_intro1 : A → (Or3 A B C)
 197 | or3_intro2 : B → (Or3 A B C)
 198 | or3_intro3 : C → (Or3 A B C).
 199
 200 nlemma or3_elim
 201  : ∀P1,P2,P3,Q:Prop.Or3 P1 P2 P3 → ∀f1:P1 → Q.∀f2:P2 → Q.∀f3:P3 → Q.Q.
 202  #P1; #P2; #P3; #Q; #H; #f1; #f2; #f3;
 203  napply (Or3_ind P1 P2 P3 ? f1 f2 f3 ?);
 204  napply H.
 205 nqed.
 206
 207 nlemma symmetric_or3_12 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P2 P1 P3.
 208  #P1; #P2; #P3; #H;
 209  napply (or3_elim P1 P2 P3 ? H);
 210  ##[ ##1: #H1; napply (or3_intro2 P2 P1 P3 H1)
 211  ##| ##2: #H1; napply (or3_intro1 P2 P1 P3 H1)
 212  ##| ##3: #H1; napply (or3_intro3 P2 P1 P3 H1)
 213  ##]
 214 nqed.
 215
 216 nlemma symmetric_or3_13 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P3 P2 P1.
 217  #P1; #P2; #P3; #H;
 218  napply (or3_elim P1 P2 P3 ? H);
 219  ##[ ##1: #H1; napply (or3_intro3 P3 P2 P1 H1)
 220  ##| ##2: #H1; napply (or3_intro2 P3 P2 P1 H1)
 221  ##| ##3: #H1; napply (or3_intro1 P3 P2 P1 H1)
 222  ##]
 223 nqed.
 224
 225 nlemma symmetric_or3_23 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P1 P3 P2.
 226  #P1; #P2; #P3; #H;
 227  napply (or3_elim P1 P2 P3 ? H);
 228  ##[ ##1: #H1; napply (or3_intro1 P1 P3 P2 H1)
 229  ##| ##2: #H1; napply (or3_intro3 P1 P3 P2 H1)
 230  ##| ##3: #H1; napply (or3_intro2 P1 P3 P2 H1)
 231  ##]
 232 nqed.
 233
 234 ninductive Or4 (A,B,C,D:Prop) : Prop ≝
 235   or4_intro1 : A → (Or4 A B C D)
 236 | or4_intro2 : B → (Or4 A B C D)
 237 | or4_intro3 : C → (Or4 A B C D)
 238 | or4_intro4 : D → (Or4 A B C D).
 239
 240 nlemma or4_elim
 241  : ∀P1,P2,P3,P4,Q:Prop.Or4 P1 P2 P3 P4 → ∀f1:P1 → Q.∀f2:P2 → Q.
 242    ∀f3:P3 → Q.∀f4:P4 → Q.Q.
 243  #P1; #P2; #P3; #P4; #Q; #H; #f1; #f2; #f3; #f4;
 244  napply (Or4_ind P1 P2 P3 P4 ? f1 f2 f3 f4 ?);
 245  napply H.
 246 nqed.
 247
 248 nlemma symmetric_or4_12 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P2 P1 P3 P4.
 249  #P1; #P2; #P3; #P4; #H;
 250  napply (or4_elim P1 P2 P3 P4 ? H);
 251  ##[ ##1: #H1; napply (or4_intro2 P2 P1 P3 P4 H1)
 252  ##| ##2: #H1; napply (or4_intro1 P2 P1 P3 P4 H1)
 253  ##| ##3: #H1; napply (or4_intro3 P2 P1 P3 P4 H1)
 254  ##| ##4: #H1; napply (or4_intro4 P2 P1 P3 P4 H1)
 255  ##]
 256 nqed.
 257
 258 nlemma symmetric_or4_13 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P3 P2 P1 P4.
 259  #P1; #P2; #P3; #P4; #H;
 260  napply (or4_elim P1 P2 P3 P4 ? H);
 261  ##[ ##1: #H1; napply (or4_intro3 P3 P2 P1 P4 H1)
 262  ##| ##2: #H1; napply (or4_intro2 P3 P2 P1 P4 H1)
 263  ##| ##3: #H1; napply (or4_intro1 P3 P2 P1 P4 H1)
 264  ##| ##4: #H1; napply (or4_intro4 P3 P2 P1 P4 H1)
 265  ##]
 266 nqed.
 267
 268 nlemma symmetric_or4_14 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P4 P2 P3 P1.
 269  #P1; #P2; #P3; #P4; #H;
 270  napply (or4_elim P1 P2 P3 P4 ? H);
 271  ##[ ##1: #H1; napply (or4_intro4 P4 P2 P3 P1 H1)
 272  ##| ##2: #H1; napply (or4_intro2 P4 P2 P3 P1 H1)
 273  ##| ##3: #H1; napply (or4_intro3 P4 P2 P3 P1 H1)
 274  ##| ##4: #H1; napply (or4_intro1 P4 P2 P3 P1 H1)
 275  ##]
 276 nqed.
 277
 278 nlemma symmetric_or4_23 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P3 P2 P4.
 279  #P1; #P2; #P3; #P4; #H;
 280  napply (or4_elim P1 P2 P3 P4 ? H);
 281  ##[ ##1: #H1; napply (or4_intro1 P1 P3 P2 P4 H1)
 282  ##| ##2: #H1; napply (or4_intro3 P1 P3 P2 P4 H1)
 283  ##| ##3: #H1; napply (or4_intro2 P1 P3 P2 P4 H1)
 284  ##| ##4: #H1; napply (or4_intro4 P1 P3 P2 P4 H1)
 285  ##]
 286 nqed.
 287
 288 nlemma symmetric_or4_24 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P4 P3 P2.
 289  #P1; #P2; #P3; #P4; #H;
 290  napply (or4_elim P1 P2 P3 P4 ? H);
 291  ##[ ##1: #H1; napply (or4_intro1 P1 P4 P3 P2 H1)
 292  ##| ##2: #H1; napply (or4_intro4 P1 P4 P3 P2 H1)
 293  ##| ##3: #H1; napply (or4_intro3 P1 P4 P3 P2 H1)
 294  ##| ##4: #H1; napply (or4_intro2 P1 P4 P3 P2 H1)
 295  ##]
 296 nqed.
 297
 298 nlemma symmetric_or4_34 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P2 P4 P3.
 299  #P1; #P2; #P3; #P4; #H;
 300  napply (or4_elim P1 P2 P3 P4 ? H);
 301  ##[ ##1: #H1; napply (or4_intro1 P1 P2 P4 P3 H1)
 302  ##| ##2: #H1; napply (or4_intro2 P1 P2 P4 P3 H1)
 303  ##| ##3: #H1; napply (or4_intro4 P1 P2 P4 P3 H1)
 304  ##| ##4: #H1; napply (or4_intro3 P1 P2 P4 P3 H1)
 305  ##]
 306 nqed.
 307
 308 ninductive Or5 (A,B,C,D,E:Prop) : Prop ≝
 309   or5_intro1 : A → (Or5 A B C D E)
 310 | or5_intro2 : B → (Or5 A B C D E)
 311 | or5_intro3 : C → (Or5 A B C D E)
 312 | or5_intro4 : D → (Or5 A B C D E)
 313 | or5_intro5 : E → (Or5 A B C D E).
 314
 315 nlemma or5_elim
 316  : ∀P1,P2,P3,P4,P5,Q:Prop.Or5 P1 P2 P3 P4 P5 → ∀f1:P1 → Q.∀f2:P2 → Q.
 317    ∀f3:P3 → Q.∀f4:P4 → Q.∀f5:P5 → Q.Q.
 318  #P1; #P2; #P3; #P4; #P5; #Q; #H; #f1; #f2; #f3; #f4; #f5;
 319  napply (Or5_ind P1 P2 P3 P4 P5 ? f1 f2 f3 f4 f5 ?);
 320  napply H.
 321 nqed.
 322
 323 nlemma symmetric_or5_12 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P2 P1 P3 P4 P5.
 324  #P1; #P2; #P3; #P4; #P5; #H;
 325  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 326  ##[ ##1: #H1; napply (or5_intro2 P2 P1 P3 P4 P5 H1)
 327  ##| ##2: #H1; napply (or5_intro1 P2 P1 P3 P4 P5 H1)
 328  ##| ##3: #H1; napply (or5_intro3 P2 P1 P3 P4 P5 H1)
 329  ##| ##4: #H1; napply (or5_intro4 P2 P1 P3 P4 P5 H1)
 330  ##| ##5: #H1; napply (or5_intro5 P2 P1 P3 P4 P5 H1)
 331  ##]
 332 nqed.
 333
 334 nlemma symmetric_or5_13 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P3 P2 P1 P4 P5.
 335  #P1; #P2; #P3; #P4; #P5; #H;
 336  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 337  ##[ ##1: #H1; napply (or5_intro3 P3 P2 P1 P4 P5 H1)
 338  ##| ##2: #H1; napply (or5_intro2 P3 P2 P1 P4 P5 H1)
 339  ##| ##3: #H1; napply (or5_intro1 P3 P2 P1 P4 P5 H1)
 340  ##| ##4: #H1; napply (or5_intro4 P3 P2 P1 P4 P5 H1)
 341  ##| ##5: #H1; napply (or5_intro5 P3 P2 P1 P4 P5 H1)
 342  ##]
 343 nqed.
 344
 345 nlemma symmetric_or5_14 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P4 P2 P3 P1 P5.
 346  #P1; #P2; #P3; #P4; #P5; #H;
 347  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 348  ##[ ##1: #H1; napply (or5_intro4 P4 P2 P3 P1 P5 H1)
 349  ##| ##2: #H1; napply (or5_intro2 P4 P2 P3 P1 P5 H1)
 350  ##| ##3: #H1; napply (or5_intro3 P4 P2 P3 P1 P5 H1)
 351  ##| ##4: #H1; napply (or5_intro1 P4 P2 P3 P1 P5 H1)
 352  ##| ##5: #H1; napply (or5_intro5 P4 P2 P3 P1 P5 H1)
 353  ##]
 354 nqed.
 355
 356 nlemma symmetric_or5_15 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P5 P2 P3 P4 P1.
 357  #P1; #P2; #P3; #P4; #P5; #H;
 358  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 359  ##[ ##1: #H1; napply (or5_intro5 P5 P2 P3 P4 P1 H1)
 360  ##| ##2: #H1; napply (or5_intro2 P5 P2 P3 P4 P1 H1)
 361  ##| ##3: #H1; napply (or5_intro3 P5 P2 P3 P4 P1 H1)
 362  ##| ##4: #H1; napply (or5_intro4 P5 P2 P3 P4 P1 H1)
 363  ##| ##5: #H1; napply (or5_intro1 P5 P2 P3 P4 P1 H1)
 364  ##]
 365 nqed.
 366
 367 nlemma symmetric_or5_23 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P3 P2 P4 P5.
 368  #P1; #P2; #P3; #P4; #P5; #H;
 369  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 370  ##[ ##1: #H1; napply (or5_intro1 P1 P3 P2 P4 P5 H1)
 371  ##| ##2: #H1; napply (or5_intro3 P1 P3 P2 P4 P5 H1)
 372  ##| ##3: #H1; napply (or5_intro2 P1 P3 P2 P4 P5 H1)
 373  ##| ##4: #H1; napply (or5_intro4 P1 P3 P2 P4 P5 H1)
 374  ##| ##5: #H1; napply (or5_intro5 P1 P3 P2 P4 P5 H1)
 375  ##]
 376 nqed.
 377
 378 nlemma symmetric_or5_24 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P4 P3 P2 P5.
 379  #P1; #P2; #P3; #P4; #P5; #H;
 380  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 381  ##[ ##1: #H1; napply (or5_intro1 P1 P4 P3 P2 P5 H1)
 382  ##| ##2: #H1; napply (or5_intro4 P1 P4 P3 P2 P5 H1)
 383  ##| ##3: #H1; napply (or5_intro3 P1 P4 P3 P2 P5 H1)
 384  ##| ##4: #H1; napply (or5_intro2 P1 P4 P3 P2 P5 H1)
 385  ##| ##5: #H1; napply (or5_intro5 P1 P4 P3 P2 P5 H1)
 386  ##]
 387 nqed.
 388
 389 nlemma symmetric_or5_25 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P5 P3 P4 P2.
 390  #P1; #P2; #P3; #P4; #P5; #H;
 391  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 392  ##[ ##1: #H1; napply (or5_intro1 P1 P5 P3 P4 P2 H1)
 393  ##| ##2: #H1; napply (or5_intro5 P1 P5 P3 P4 P2 H1)
 394  ##| ##3: #H1; napply (or5_intro3 P1 P5 P3 P4 P2 H1)
 395  ##| ##4: #H1; napply (or5_intro4 P1 P5 P3 P4 P2 H1)
 396  ##| ##5: #H1; napply (or5_intro2 P1 P5 P3 P4 P2 H1)
 397  ##]
 398 nqed.
 399
 400 nlemma symmetric_or5_34 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P4 P3 P5.
 401  #P1; #P2; #P3; #P4; #P5; #H;
 402  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 403  ##[ ##1: #H1; napply (or5_intro1 P1 P2 P4 P3 P5 H1)
 404  ##| ##2: #H1; napply (or5_intro2 P1 P2 P4 P3 P5 H1)
 405  ##| ##3: #H1; napply (or5_intro4 P1 P2 P4 P3 P5 H1)
 406  ##| ##4: #H1; napply (or5_intro3 P1 P2 P4 P3 P5 H1)
 407  ##| ##5: #H1; napply (or5_intro5 P1 P2 P4 P3 P5 H1)
 408  ##]
 409 nqed.
 410
 411 nlemma symmetric_or5_35 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P5 P4 P3.
 412  #P1; #P2; #P3; #P4; #P5; #H;
 413  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 414  ##[ ##1: #H1; napply (or5_intro1 P1 P2 P5 P4 P3 H1)
 415  ##| ##2: #H1; napply (or5_intro2 P1 P2 P5 P4 P3 H1)
 416  ##| ##3: #H1; napply (or5_intro5 P1 P2 P5 P4 P3 H1)
 417  ##| ##4: #H1; napply (or5_intro4 P1 P2 P5 P4 P3 H1)
 418  ##| ##5: #H1; napply (or5_intro3 P1 P2 P5 P4 P3 H1)
 419  ##]
 420 nqed.
 421
 422 nlemma symmetric_or5_45 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P3 P5 P4.
 423  #P1; #P2; #P3; #P4; #P5; #H;
 424  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 425  ##[ ##1: #H1; napply (or5_intro1 P1 P2 P3 P5 P4 H1)
 426  ##| ##2: #H1; napply (or5_intro2 P1 P2 P3 P5 P4 H1)
 427  ##| ##3: #H1; napply (or5_intro3 P1 P2 P3 P5 P4 H1)
 428  ##| ##4: #H1; napply (or5_intro5 P1 P2 P3 P5 P4 H1)
 429  ##| ##5: #H1; napply (or5_intro4 P1 P2 P3 P5 P4 H1)
 430  ##]
 431 nqed.
 432
 433 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
 434  ex_intro: ∀x:A.Q x → ex A Q.
 435
 436 interpretation "exists" 'exists x = (ex ? x).
 437
 438 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
 439  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
 440
 441 (* higher_order_defs/relations *)
 442
 443 ndefinition relation : Type → Type ≝
 444 λA.A → A → Prop.
 445
 446 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
 447 λA.λR.∀x:A.R x x.
 448
 449 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
 450 λA.λR.∀x,y:A.R x y → R y x.
 451
 452 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
 453 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
 454
 455 ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
 456 λA.λR.∀x:A.¬ (R x x).
 457
 458 ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
 459 λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
 460
 461 ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
 462 λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
 463
 464 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
 465 λA.λR.∀x,y:A.R x y → ¬ (R y x).
 466
 467 (* logic/equality.ma *)
 468
 469 ninductive eq (A:Type) (x:A) : A → Prop ≝
 470  refl_eq : eq A x x.
 471
 472 ndefinition refl ≝ refl_eq.
 473
 474 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 475
 476 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
 477
 478 nlemma eq_f : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.x = y → (f x) = (f y).
 479  #T1; #T2; #x; #y; #f; #H;
 480  nrewrite < H;
 481  napply refl_eq.
 482 nqed.
 483
 484 nlemma eq_f2 : ∀T1,T2,T3:Type.∀x1,y1:T1.∀x2,y2:T2.∀f:T1 → T2 → T3.x1 = y1 → x2 = y2 → f x1 x2 = f y1 y2.
 485  #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; #H1; #H2;
 486  nrewrite < H1;
 487  nrewrite < H2;
 488  napply refl_eq.
 489 nqed.
 490
 491 nlemma neqf_to_neq : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.((f x) ≠ (f y)) → x ≠ y.
 492  #T1; #T2; #x; #y; #f;
 493  nnormalize; #H; #H1;
 494  napply (H (eq_f … H1)).
 495 nqed.
 496
 497 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
 498  #A;
 499  nnormalize;
 500  #x; #y; #H;
 501  nrewrite < H;
 502  napply refl_eq.
 503 nqed.
 504
 505 nlemma eq_ind_r: ∀A:Type[0].∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
 506  #A; #x; #P; #H; #y; #H1;
 507  nrewrite < (symmetric_eq … H1);
 508  napply H.
 509 nqed.
 510
 511 ndefinition R0 ≝ λT:Type[0].λt:T.t.
 512
 513 ndefinition R1 ≝ eq_rect_Type0.
 514
 515 ndefinition R2 :
 516   ∀T0:Type[0].
 517   ∀a0:T0.
 518   ∀T1:∀x0:T0. a0=x0 → Type[0].
 519   ∀a1:T1 a0 (refl_eq ? a0).
 520   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
 521   ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
 522   ∀b0:T0.
 523   ∀e0:a0 = b0.
 524   ∀b1: T1 b0 e0.
 525   ∀e1:R1 ?? T1 a1 ? e0 = b1.
 526   T2 b0 e0 b1 e1.
 527  #T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
 528  napply (eq_rect_Type0 ????? e1);
 529  napply (R1 ?? ? ?? e0);
 530  napply a2;
 531 nqed.
 532
 533 ndefinition R3 :
 534   ∀T0:Type[0].
 535   ∀a0:T0.
 536   ∀T1:∀x0:T0. a0=x0 → Type[0].
 537   ∀a1:T1 a0 (refl_eq ? a0).
 538   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
 539   ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
 540   ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
 541       ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
 542   ∀a3:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).
 543   ∀b0:T0.
 544   ∀e0:a0 = b0.
 545   ∀b1: T1 b0 e0.
 546   ∀e1:R1 ?? T1 a1 ? e0 = b1.
 547   ∀b2: T2 b0 e0 b1 e1.
 548   ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
 549   T3 b0 e0 b1 e1 b2 e2.
 550  #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
 551  napply (eq_rect_Type0 ????? e2);
 552  napply (R2 ?? ? ???? e0 ? e1);
 553  napply a3;
 554 nqed.
 555
 556 ndefinition R4 :
 557   ∀T0:Type[0].
 558   ∀a0:T0.
 559   ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
 560   ∀a1:T1 a0 (refl_eq T0 a0).
 561   ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
 562   ∀a2:T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1).
 563   ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 564       ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
 565   ∀a3:T3 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)
 566       a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2).
 567   ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 568       ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
 569       ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3.
 570       Type[0].
 571   ∀a4:T4 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)
 572       a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2)
 573       a3 (refl_eq (T3 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)
 574                    a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2))
 575                    a3).
 576   ∀b0:T0.
 577   ∀e0:eq (T0 …) a0 b0.
 578   ∀b1: T1 b0 e0.
 579   ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
 580   ∀b2: T2 b0 e0 b1 e1.
 581   ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
 582   ∀b3: T3 b0 e0 b1 e1 b2 e2.
 583   ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
 584   T4 b0 e0 b1 e1 b2 e2 b3 e3.
 585  #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
 586  napply (eq_rect_Type0 ????? e3);
 587  napply (R3 ????????? e0 ? e1 ? e2);
 588  napply a4;
 589 nqed.
 590
 591 naxiom streicherK : ∀T:Type[0].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.
 592
 593 nlemma symmetric_neq : ∀T:Type.∀x,y:T.x ≠ y → y ≠ x.
 594  #T; #x; #y;
 595  nnormalize;
 596  #H; #H1;
 597  nrewrite > H1 in H:(%); #H;
 598  napply (H (refl_eq …)).
 599 nqed.
 600
 601 ndefinition relationT : Type → Type → Type ≝
 602 λA,T:Type.A → A → T.
 603
 604 ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
 605 λA,T.λR.∀x,y:A.R x y = R y x.
 606
 607 ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
 608 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).