helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/dec.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/subst0/dec".
  18
  19 include "subst0/defs.ma".
  20
  21 include "lift/props.ma".
  22
  23 theorem dnf_dec:
  24  \forall (w: T).(\forall (t: T).(\forall (d: nat).(ex T (\lambda (v: T).(or
  25 (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v)))))))
  26 \def
  27  \lambda (w: T).(\lambda (t: T).(\lambda (d: nat).(let H_x \def (dnf_dec2 t
  28 d) in (let H \def H_x in (or_ind (\forall (w0: T).(ex T (\lambda (v:
  29 T).(subst0 d w0 t (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T t (lift (S
  30 O) d v)))) (ex T (\lambda (v: T).(or (subst0 d w t (lift (S O) d v)) (eq T t
  31 (lift (S O) d v))))) (\lambda (H0: ((\forall (w0: T).(ex T (\lambda (v:
  32 T).(subst0 d w0 t (lift (S O) d v))))))).(let H_x0 \def (H0 w) in (let H1
  33 \def H_x0 in (ex_ind T (\lambda (v: T).(subst0 d w t (lift (S O) d v))) (ex T
  34 (\lambda (v: T).(or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d
  35 v))))) (\lambda (x: T).(\lambda (H2: (subst0 d w t (lift (S O) d
  36 x))).(ex_intro T (\lambda (v: T).(or (subst0 d w t (lift (S O) d v)) (eq T t
  37 (lift (S O) d v)))) x (or_introl (subst0 d w t (lift (S O) d x)) (eq T t
  38 (lift (S O) d x)) H2)))) H1)))) (\lambda (H0: (ex T (\lambda (v: T).(eq T t
  39 (lift (S O) d v))))).(ex_ind T (\lambda (v: T).(eq T t (lift (S O) d v))) (ex
  40 T (\lambda (v: T).(or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d
  41 v))))) (\lambda (x: T).(\lambda (H1: (eq T t (lift (S O) d x))).(eq_ind_r T
  42 (lift (S O) d x) (\lambda (t0: T).(ex T (\lambda (v: T).(or (subst0 d w t0
  43 (lift (S O) d v)) (eq T t0 (lift (S O) d v)))))) (ex_intro T (\lambda (v:
  44 T).(or (subst0 d w (lift (S O) d x) (lift (S O) d v)) (eq T (lift (S O) d x)
  45 (lift (S O) d v)))) x (or_intror (subst0 d w (lift (S O) d x) (lift (S O) d
  46 x)) (eq T (lift (S O) d x) (lift (S O) d x)) (refl_equal T (lift (S O) d
  47 x)))) t H1))) H0)) H))))).
  48