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