1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/dec".
19 include "subst0/defs.ma".
21 include "lift/props.ma".
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)))))))
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))))).