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