(* This file was automatically generated: do not edit *********************)
-include "pr0/fwd.ma".
+include "LambdaDelta-1/pr0/fwd.ma".
-include "subst0/dec.ma".
+include "LambdaDelta-1/subst0/dec.ma".
-include "T/dec.ma".
+include "LambdaDelta-1/T/dec.ma".
-include "T/props.ma".
+include "LambdaDelta-1/T/props.ma".
theorem nf0_dec:
\forall (t1: T).(or (\forall (t2: T).((pr0 t1 t2) \to (eq T t1 t2))) (ex2 T