(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/subst0/defs.ma".
+include "Basic-1/subst0/defs.ma".
-include "LambdaDelta-1/lift/props.ma".
+include "Basic-1/lift/props.ma".
theorem dnf_dec2:
\forall (t: T).(\forall (d: nat).(or (\forall (w: T).(ex T (\lambda (v:
(lift (S O) (s k d) x0)) t2)) (refl_equal T (THead k (lift (S O) d x) (lift
(S O) (s k d) x0))) (lift (S O) d (THead k x x0)) (lift_head k x x0 (S O)
d)))) t0 H3) t1 H6))) H5)) H4))))) H2)) H1))))))))) t).
+(* COMMENTS
+Initial nodes: 3549
+END *)
theorem dnf_dec:
\forall (w: T).(\forall (t: T).(\forall (d: nat).(ex T (\lambda (v: T).(or
(lift (S O) d v)))) x (or_intror (subst0 d w (lift (S O) d x) (lift (S O) d
x)) (eq T (lift (S O) d x) (lift (S O) d x)) (refl_equal T (lift (S O) d
x)))) t H1))) H0)) H))))).
+(* COMMENTS
+Initial nodes: 603
+END *)