| 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)))).