matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/cnt.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
  18
  19 include "tau1/props.ma".
  20
  21 include "cnt/props.ma".
  22
  23 theorem tau1_cnt:
  24  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t: T).((tau0 g c
  25 t1 t) \to (ex2 T (\lambda (t2: T).(tau1 g c t1 t2)) (\lambda (t2: T).(cnt
  26 t2)))))))
  27 \def
  28  \lambda (g: G).(\lambda (c: C).(\lambda (t1: T).(\lambda (t: T).(\lambda (H:
  29 (tau0 g c t1 t)).(tau0_ind g (\lambda (c0: C).(\lambda (t0: T).(\lambda (_:
  30 T).(ex2 T (\lambda (t3: T).(tau1 g c0 t0 t3)) (\lambda (t3: T).(cnt t3))))))
  31 (\lambda (c0: C).(\lambda (n: nat).(ex_intro2 T (\lambda (t2: T).(tau1 g c0
  32 (TSort n) t2)) (\lambda (t2: T).(cnt t2)) (TSort (next g n)) (tau1_tau0 g c0
  33 (TSort n) (TSort (next g n)) (tau0_sort g c0 n)) (cnt_sort (next g n)))))
  34 (\lambda (c0: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda
  35 (H0: (getl i c0 (CHead d (Bind Abbr) v))).(\lambda (w: T).(\lambda (_: (tau0
  36 g d v w)).(\lambda (H2: (ex2 T (\lambda (t2: T).(tau1 g d v t2)) (\lambda
  37 (t2: T).(cnt t2)))).(let H3 \def H2 in (ex2_ind T (\lambda (t2: T).(tau1 g d
  38 v t2)) (\lambda (t2: T).(cnt t2)) (ex2 T (\lambda (t2: T).(tau1 g c0 (TLRef
  39 i) t2)) (\lambda (t2: T).(cnt t2))) (\lambda (x: T).(\lambda (H4: (tau1 g d v
  40 x)).(\lambda (H5: (cnt x)).(ex_intro2 T (\lambda (t2: T).(tau1 g c0 (TLRef i)
  41 t2)) (\lambda (t2: T).(cnt t2)) (lift (S i) O x) (tau1_abbr g c0 d v i H0 x
  42 H4) (cnt_lift x H5 (S i) O))))) H3)))))))))) (\lambda (c0: C).(\lambda (d:
  43 C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H0: (getl i c0 (CHead d (Bind
  44 Abst) v))).(\lambda (w: T).(\lambda (H1: (tau0 g d v w)).(\lambda (H2: (ex2 T
  45 (\lambda (t2: T).(tau1 g d v t2)) (\lambda (t2: T).(cnt t2)))).(let H3 \def
  46 H2 in (ex2_ind T (\lambda (t2: T).(tau1 g d v t2)) (\lambda (t2: T).(cnt t2))
  47 (ex2 T (\lambda (t2: T).(tau1 g c0 (TLRef i) t2)) (\lambda (t2: T).(cnt t2)))
  48 (\lambda (x: T).(\lambda (H4: (tau1 g d v x)).(\lambda (H5: (cnt
  49 x)).(ex_intro2 T (\lambda (t2: T).(tau1 g c0 (TLRef i) t2)) (\lambda (t2:
  50 T).(cnt t2)) (lift (S i) O x) (tau1_trans g c0 (TLRef i) (lift (S i) O v)
  51 (tau1_tau0 g c0 (TLRef i) (lift (S i) O v) (tau0_abst g c0 d v i H0 w H1))
  52 (lift (S i) O x) (tau1_lift g d v x H4 c0 (S i) O (getl_drop Abst c0 d v i
  53 H0))) (cnt_lift x H5 (S i) O))))) H3)))))))))) (\lambda (b: B).(\lambda (c0:
  54 C).(\lambda (v: T).(\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (tau0 g
  55 (CHead c0 (Bind b) v) t2 t3)).(\lambda (H1: (ex2 T (\lambda (t4: T).(tau1 g
  56 (CHead c0 (Bind b) v) t2 t4)) (\lambda (t4: T).(cnt t4)))).(let H2 \def H1 in
  57 (ex2_ind T (\lambda (t4: T).(tau1 g (CHead c0 (Bind b) v) t2 t4)) (\lambda
  58 (t4: T).(cnt t4)) (ex2 T (\lambda (t4: T).(tau1 g c0 (THead (Bind b) v t2)
  59 t4)) (\lambda (t4: T).(cnt t4))) (\lambda (x: T).(\lambda (H3: (tau1 g (CHead
  60 c0 (Bind b) v) t2 x)).(\lambda (H4: (cnt x)).(ex_intro2 T (\lambda (t4:
  61 T).(tau1 g c0 (THead (Bind b) v t2) t4)) (\lambda (t4: T).(cnt t4)) (THead
  62 (Bind b) v x) (tau1_bind g b c0 v t2 x H3) (cnt_head x H4 (Bind b) v)))))
  63 H2))))))))) (\lambda (c0: C).(\lambda (v: T).(\lambda (t2: T).(\lambda (t3:
  64 T).(\lambda (_: (tau0 g c0 t2 t3)).(\lambda (H1: (ex2 T (\lambda (t4:
  65 T).(tau1 g c0 t2 t4)) (\lambda (t4: T).(cnt t4)))).(let H2 \def H1 in
  66 (ex2_ind T (\lambda (t4: T).(tau1 g c0 t2 t4)) (\lambda (t4: T).(cnt t4))
  67 (ex2 T (\lambda (t4: T).(tau1 g c0 (THead (Flat Appl) v t2) t4)) (\lambda
  68 (t4: T).(cnt t4))) (\lambda (x: T).(\lambda (H3: (tau1 g c0 t2 x)).(\lambda
  69 (H4: (cnt x)).(ex_intro2 T (\lambda (t4: T).(tau1 g c0 (THead (Flat Appl) v
  70 t2) t4)) (\lambda (t4: T).(cnt t4)) (THead (Flat Appl) v x) (tau1_appl g c0 v
  71 t2 x H3) (cnt_head x H4 (Flat Appl) v))))) H2)))))))) (\lambda (c0:
  72 C).(\lambda (v1: T).(\lambda (v2: T).(\lambda (H0: (tau0 g c0 v1
  73 v2)).(\lambda (_: (ex2 T (\lambda (t2: T).(tau1 g c0 v1 t2)) (\lambda (t2:
  74 T).(cnt t2)))).(\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (tau0 g c0 t2
  75 t3)).(\lambda (H3: (ex2 T (\lambda (t4: T).(tau1 g c0 t2 t4)) (\lambda (t4:
  76 T).(cnt t4)))).(let H4 \def H3 in (ex2_ind T (\lambda (t4: T).(tau1 g c0 t2
  77 t4)) (\lambda (t4: T).(cnt t4)) (ex2 T (\lambda (t4: T).(tau1 g c0 (THead
  78 (Flat Cast) v1 t2) t4)) (\lambda (t4: T).(cnt t4))) (\lambda (x: T).(\lambda
  79 (H5: (tau1 g c0 t2 x)).(\lambda (H6: (cnt x)).(let H_x \def (tau1_cast2 g c0
  80 t2 x H5 v1 v2 H0) in (let H7 \def H_x in (ex2_ind T (\lambda (v3: T).(tau1 g
  81 c0 v1 v3)) (\lambda (v3: T).(tau1 g c0 (THead (Flat Cast) v1 t2) (THead (Flat
  82 Cast) v3 x))) (ex2 T (\lambda (t4: T).(tau1 g c0 (THead (Flat Cast) v1 t2)
  83 t4)) (\lambda (t4: T).(cnt t4))) (\lambda (x0: T).(\lambda (_: (tau1 g c0 v1
  84 x0)).(\lambda (H9: (tau1 g c0 (THead (Flat Cast) v1 t2) (THead (Flat Cast) x0
  85 x))).(ex_intro2 T (\lambda (t4: T).(tau1 g c0 (THead (Flat Cast) v1 t2) t4))
  86 (\lambda (t4: T).(cnt t4)) (THead (Flat Cast) x0 x) H9 (cnt_head x H6 (Flat
  87 Cast) x0))))) H7)))))) H4))))))))))) c t1 t H))))).
  88