helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/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/T/props".
  18
  19 include "T/defs.ma".
  20
  21 theorem not_abbr_abst:
  22  not (eq B Abbr Abst)
  23 \def
  24  \lambda (H: (eq B Abbr Abst)).(let H0 \def (eq_ind B Abbr (\lambda (ee:
  25 B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow True |
  26 Abst \Rightarrow False | Void \Rightarrow False])) I Abst H) in (False_ind
  27 False H0)).
  28
  29 theorem not_void_abst:
  30  not (eq B Void Abst)
  31 \def
  32  \lambda (H: (eq B Void Abst)).(let H0 \def (eq_ind B Void (\lambda (ee:
  33 B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow False |
  34 Abst \Rightarrow False | Void \Rightarrow True])) I Abst H) in (False_ind
  35 False H0)).
  36
  37 theorem thead_x_y_y:
  38  \forall (k: K).(\forall (v: T).(\forall (t: T).((eq T (THead k v t) t) \to
  39 (\forall (P: Prop).P))))
  40 \def
  41  \lambda (k: K).(\lambda (v: T).(\lambda (t: T).(T_ind (\lambda (t0: T).((eq
  42 T (THead k v t0) t0) \to (\forall (P: Prop).P))) (\lambda (n: nat).(\lambda
  43 (H: (eq T (THead k v (TSort n)) (TSort n))).(\lambda (P: Prop).(let H0 \def
  44 (eq_ind T (THead k v (TSort n)) (\lambda (ee: T).(match ee in T return
  45 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
  46 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H) in
  47 (False_ind P H0))))) (\lambda (n: nat).(\lambda (H: (eq T (THead k v (TLRef
  48 n)) (TLRef n))).(\lambda (P: Prop).(let H0 \def (eq_ind T (THead k v (TLRef
  49 n)) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort
  50 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
  51 \Rightarrow True])) I (TLRef n) H) in (False_ind P H0))))) (\lambda (k0:
  52 K).(\lambda (t0: T).(\lambda (_: (((eq T (THead k v t0) t0) \to (\forall (P:
  53 Prop).P)))).(\lambda (t1: T).(\lambda (H0: (((eq T (THead k v t1) t1) \to
  54 (\forall (P: Prop).P)))).(\lambda (H1: (eq T (THead k v (THead k0 t0 t1))
  55 (THead k0 t0 t1))).(\lambda (P: Prop).(let H2 \def (f_equal T K (\lambda (e:
  56 T).(match e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k |
  57 (TLRef _) \Rightarrow k | (THead k _ _) \Rightarrow k])) (THead k v (THead k0
  58 t0 t1)) (THead k0 t0 t1) H1) in ((let H3 \def (f_equal T T (\lambda (e:
  59 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v |
  60 (TLRef _) \Rightarrow v | (THead _ t _) \Rightarrow t])) (THead k v (THead k0
  61 t0 t1)) (THead k0 t0 t1) H1) in ((let H4 \def (f_equal T T (\lambda (e:
  62 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow (THead
  63 k0 t0 t1) | (TLRef _) \Rightarrow (THead k0 t0 t1) | (THead _ _ t)
  64 \Rightarrow t])) (THead k v (THead k0 t0 t1)) (THead k0 t0 t1) H1) in
  65 (\lambda (H5: (eq T v t0)).(\lambda (H6: (eq K k k0)).(let H7 \def (eq_ind T
  66 v (\lambda (t: T).((eq T (THead k t t1) t1) \to (\forall (P: Prop).P))) H0 t0
  67 H5) in (let H8 \def (eq_ind K k (\lambda (k: K).((eq T (THead k t0 t1) t1)
  68 \to (\forall (P: Prop).P))) H7 k0 H6) in (H8 H4 P)))))) H3)) H2))))))))) t))).
  69
  70 theorem tweight_lt:
  71  \forall (t: T).(lt O (tweight t))
  72 \def
  73  \lambda (t: T).(match t in T return (\lambda (t0: T).(lt O (tweight t0)))
  74 with [(TSort _) \Rightarrow (le_n (S O)) | (TLRef _) \Rightarrow (le_n (S O))
  75 | (THead _ t0 t1) \Rightarrow (le_S_n (S O) (S (plus (tweight t0) (tweight
  76 t1))) (le_n_S (S O) (S (plus (tweight t0) (tweight t1))) (le_n_S O (plus
  77 (tweight t0) (tweight t1)) (le_O_n (plus (tweight t0) (tweight t1))))))]).
  78