(* This file was automatically generated: do not edit *********************)
-include "subst0/defs.ma".
+include "LambdaDelta-1/subst0/defs.ma".
inductive pr0: T \to (T \to Prop) \def
| pr0_refl: \forall (t: T).(pr0 t t)
| pr0_zeta: \forall (b: B).((not (eq B b Abst)) \to (\forall (t1: T).(\forall
(t2: T).((pr0 t1 t2) \to (\forall (u: T).(pr0 (THead (Bind b) u (lift (S O) O
t1)) t2))))))
-| pr0_epsilon: \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (u:
+| pr0_tau: \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (u:
T).(pr0 (THead (Flat Cast) u t1) t2)))).