helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/props.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/props".
  18
  19 include "pr1/defs.ma".
  20
  21 theorem pr1_pr0:
  22  \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (pr1 t1 t2)))
  23 \def
  24  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t1 t2)).(pr1_u t2 t1 H t2
  25 (pr1_r t2)))).
  26
  27 theorem pr1_t:
  28  \forall (t2: T).(\forall (t1: T).((pr1 t1 t2) \to (\forall (t3: T).((pr1 t2
  29 t3) \to (pr1 t1 t3)))))
  30 \def
  31  \lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pr1 t1 t2)).(pr1_ind (\lambda
  32 (t: T).(\lambda (t0: T).(\forall (t3: T).((pr1 t0 t3) \to (pr1 t t3)))))
  33 (\lambda (t: T).(\lambda (t3: T).(\lambda (H0: (pr1 t t3)).H0))) (\lambda
  34 (t0: T).(\lambda (t3: T).(\lambda (H0: (pr0 t3 t0)).(\lambda (t4: T).(\lambda
  35 (_: (pr1 t0 t4)).(\lambda (H2: ((\forall (t5: T).((pr1 t4 t5) \to (pr1 t0
  36 t5))))).(\lambda (t5: T).(\lambda (H3: (pr1 t4 t5)).(pr1_u t0 t3 H0 t5 (H2 t5
  37 H3)))))))))) t1 t2 H))).
  38
  39 theorem pr1_head_1:
  40  \forall (u1: T).(\forall (u2: T).((pr1 u1 u2) \to (\forall (t: T).(\forall
  41 (k: K).(pr1 (THead k u1 t) (THead k u2 t))))))
  42 \def
  43  \lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pr1 u1 u2)).(\lambda (t:
  44 T).(\lambda (k: K).(pr1_ind (\lambda (t0: T).(\lambda (t1: T).(pr1 (THead k
  45 t0 t) (THead k t1 t)))) (\lambda (t0: T).(pr1_r (THead k t0 t))) (\lambda
  46 (t2: T).(\lambda (t1: T).(\lambda (H0: (pr0 t1 t2)).(\lambda (t3: T).(\lambda
  47 (_: (pr1 t2 t3)).(\lambda (H2: (pr1 (THead k t2 t) (THead k t3 t))).(pr1_u
  48 (THead k t2 t) (THead k t1 t) (pr0_comp t1 t2 H0 t t (pr0_refl t) k) (THead k
  49 t3 t) H2))))))) u1 u2 H))))).
  50
  51 theorem pr1_head_2:
  52  \forall (t1: T).(\forall (t2: T).((pr1 t1 t2) \to (\forall (u: T).(\forall
  53 (k: K).(pr1 (THead k u t1) (THead k u t2))))))
  54 \def
  55  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr1 t1 t2)).(\lambda (u:
  56 T).(\lambda (k: K).(pr1_ind (\lambda (t: T).(\lambda (t0: T).(pr1 (THead k u
  57 t) (THead k u t0)))) (\lambda (t: T).(pr1_r (THead k u t))) (\lambda (t0:
  58 T).(\lambda (t3: T).(\lambda (H0: (pr0 t3 t0)).(\lambda (t4: T).(\lambda (_:
  59 (pr1 t0 t4)).(\lambda (H2: (pr1 (THead k u t0) (THead k u t4))).(pr1_u (THead
  60 k u t0) (THead k u t3) (pr0_comp u u (pr0_refl u) t3 t0 H0 k) (THead k u t4)
  61 H2))))))) t1 t2 H))))).
  62