matita/matita/contribs/lambdadelta/basic_1A/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 include "basic_1A/T/fwd.ma".
  18
  19 lemma not_abbr_abst:
  20  not (eq B Abbr Abst)
  21 \def
  22  \lambda (H: (eq B Abbr Abst)).(let H0 \def (eq_ind B Abbr (\lambda (ee:
  23 B).(match ee with [Abbr \Rightarrow True | Abst \Rightarrow False | Void
  24 \Rightarrow False])) I Abst H) in (False_ind False H0)).
  25
  26 lemma not_void_abst:
  27  not (eq B Void Abst)
  28 \def
  29  \lambda (H: (eq B Void Abst)).(let H0 \def (eq_ind B Void (\lambda (ee:
  30 B).(match ee with [Abbr \Rightarrow False | Abst \Rightarrow False | Void
  31 \Rightarrow True])) I Abst H) in (False_ind False H0)).
  32
  33 lemma not_abbr_void:
  34  not (eq B Abbr Void)
  35 \def
  36  \lambda (H: (eq B Abbr Void)).(let H0 \def (eq_ind B Abbr (\lambda (ee:
  37 B).(match ee with [Abbr \Rightarrow True | Abst \Rightarrow False | Void
  38 \Rightarrow False])) I Void H) in (False_ind False H0)).
  39
  40 lemma not_abst_void:
  41  not (eq B Abst Void)
  42 \def
  43  \lambda (H: (eq B Abst Void)).(let H0 \def (eq_ind B Abst (\lambda (ee:
  44 B).(match ee with [Abbr \Rightarrow False | Abst \Rightarrow True | Void
  45 \Rightarrow False])) I Void H) in (False_ind False H0)).
  46
  47 lemma tweight_lt:
  48  \forall (t: T).(lt O (tweight t))
  49 \def
  50  \lambda (t: T).(T_ind (\lambda (t0: T).(lt O (tweight t0))) (\lambda (_:
  51 nat).(le_n (S O))) (\lambda (_: nat).(le_n (S O))) (\lambda (_: K).(\lambda
  52 (t0: T).(\lambda (H: (lt O (tweight t0))).(\lambda (t1: T).(\lambda (_: (lt O
  53 (tweight t1))).(le_S (S O) (plus (tweight t0) (tweight t1)) (le_plus_trans (S
  54 O) (tweight t0) (tweight t1) H))))))) t).
  55
  56 lemma tle_r:
  57  \forall (t: T).(tle t t)
  58 \def
  59  \lambda (t: T).(T_ind (\lambda (t0: T).(le (tweight t0) (tweight t0)))
  60 (\lambda (_: nat).(le_n (S O))) (\lambda (_: nat).(le_n (S O))) (\lambda (_:
  61 K).(\lambda (t0: T).(\lambda (_: (le (tweight t0) (tweight t0))).(\lambda
  62 (t1: T).(\lambda (_: (le (tweight t1) (tweight t1))).(le_n (S (plus (tweight
  63 t0) (tweight t1))))))))) t).
  64