-let rec pr0_ind (P: (T \to (T \to Prop))) (f: (\forall (t: T).(P t t))) (f0:
-(\forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to ((P u1 u2) \to (\forall
-(t1: T).(\forall (t2: T).((pr0 t1 t2) \to ((P t1 t2) \to (\forall (k: K).(P
-(THead k u1 t1) (THead k u2 t2)))))))))))) (f1: (\forall (u: T).(\forall (v1:
-T).(\forall (v2: T).((pr0 v1 v2) \to ((P v1 v2) \to (\forall (t1: T).(\forall
-(t2: T).((pr0 t1 t2) \to ((P t1 t2) \to (P (THead (Flat Appl) v1 (THead (Bind
-Abst) u t1)) (THead (Bind Abbr) v2 t2)))))))))))) (f2: (\forall (b: B).((not
-(eq B b Abst)) \to (\forall (v1: T).(\forall (v2: T).((pr0 v1 v2) \to ((P v1
-v2) \to (\forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to ((P u1 u2) \to
-(\forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to ((P t1 t2) \to (P (THead
-(Flat Appl) v1 (THead (Bind b) u1 t1)) (THead (Bind b) u2 (THead (Flat Appl)
-(lift (S O) O v2) t2)))))))))))))))))) (f3: (\forall (u1: T).(\forall (u2:
-T).((pr0 u1 u2) \to ((P u1 u2) \to (\forall (t1: T).(\forall (t2: T).((pr0 t1
-t2) \to ((P t1 t2) \to (\forall (w: T).((subst0 O u2 t2 w) \to (P (THead
-(Bind Abbr) u1 t1) (THead (Bind Abbr) u2 w))))))))))))) (f4: (\forall (b:
-B).((not (eq B b Abst)) \to (\forall (t1: T).(\forall (t2: T).((pr0 t1 t2)
-\to ((P t1 t2) \to (\forall (u: T).(P (THead (Bind b) u (lift (S O) O t1))
-t2))))))))) (f5: (\forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to ((P t1
-t2) \to (\forall (u: T).(P (THead (Flat Cast) u t1) t2))))))) (t: T) (t0: T)
-(p: pr0 t t0) on p: P t t0 \def match p with [(pr0_refl t1) \Rightarrow (f
-t1) | (pr0_comp u1 u2 p0 t1 t2 p1 k) \Rightarrow (f0 u1 u2 p0 ((pr0_ind P f
-f0 f1 f2 f3 f4 f5) u1 u2 p0) t1 t2 p1 ((pr0_ind P f f0 f1 f2 f3 f4 f5) t1 t2
-p1) k) | (pr0_beta u v1 v2 p0 t1 t2 p1) \Rightarrow (f1 u v1 v2 p0 ((pr0_ind
-P f f0 f1 f2 f3 f4 f5) v1 v2 p0) t1 t2 p1 ((pr0_ind P f f0 f1 f2 f3 f4 f5) t1
-t2 p1)) | (pr0_upsilon b n v1 v2 p0 u1 u2 p1 t1 t2 p2) \Rightarrow (f2 b n v1
-v2 p0 ((pr0_ind P f f0 f1 f2 f3 f4 f5) v1 v2 p0) u1 u2 p1 ((pr0_ind P f f0 f1
-f2 f3 f4 f5) u1 u2 p1) t1 t2 p2 ((pr0_ind P f f0 f1 f2 f3 f4 f5) t1 t2 p2)) |
-(pr0_delta u1 u2 p0 t1 t2 p1 w s0) \Rightarrow (f3 u1 u2 p0 ((pr0_ind P f f0
-f1 f2 f3 f4 f5) u1 u2 p0) t1 t2 p1 ((pr0_ind P f f0 f1 f2 f3 f4 f5) t1 t2 p1)
-w s0) | (pr0_zeta b n t1 t2 p0 u) \Rightarrow (f4 b n t1 t2 p0 ((pr0_ind P f
-f0 f1 f2 f3 f4 f5) t1 t2 p0) u) | (pr0_tau t1 t2 p0 u) \Rightarrow (f5 t1 t2
-p0 ((pr0_ind P f f0 f1 f2 f3 f4 f5) t1 t2 p0) u)].
+implied let rec pr0_ind (P: (T \to (T \to Prop))) (f: (\forall (t: T).(P t
+t))) (f0: (\forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to ((P u1 u2) \to
+(\forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to ((P t1 t2) \to (\forall
+(k: K).(P (THead k u1 t1) (THead k u2 t2)))))))))))) (f1: (\forall (u:
+T).(\forall (v1: T).(\forall (v2: T).((pr0 v1 v2) \to ((P v1 v2) \to (\forall
+(t1: T).(\forall (t2: T).((pr0 t1 t2) \to ((P t1 t2) \to (P (THead (Flat
+Appl) v1 (THead (Bind Abst) u t1)) (THead (Bind Abbr) v2 t2)))))))))))) (f2:
+(\forall (b: B).((not (eq B b Abst)) \to (\forall (v1: T).(\forall (v2:
+T).((pr0 v1 v2) \to ((P v1 v2) \to (\forall (u1: T).(\forall (u2: T).((pr0 u1
+u2) \to ((P u1 u2) \to (\forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to ((P
+t1 t2) \to (P (THead (Flat Appl) v1 (THead (Bind b) u1 t1)) (THead (Bind b)
+u2 (THead (Flat Appl) (lift (S O) O v2) t2)))))))))))))))))) (f3: (\forall
+(u1: T).(\forall (u2: T).((pr0 u1 u2) \to ((P u1 u2) \to (\forall (t1:
+T).(\forall (t2: T).((pr0 t1 t2) \to ((P t1 t2) \to (\forall (w: T).((subst0
+O u2 t2 w) \to (P (THead (Bind Abbr) u1 t1) (THead (Bind Abbr) u2
+w))))))))))))) (f4: (\forall (b: B).((not (eq B b Abst)) \to (\forall (t1:
+T).(\forall (t2: T).((pr0 t1 t2) \to ((P t1 t2) \to (\forall (u: T).(P (THead
+(Bind b) u (lift (S O) O t1)) t2))))))))) (f5: (\forall (t1: T).(\forall (t2:
+T).((pr0 t1 t2) \to ((P t1 t2) \to (\forall (u: T).(P (THead (Flat Cast) u
+t1) t2))))))) (t: T) (t0: T) (p: pr0 t t0) on p: P t t0 \def match p with
+[(pr0_refl t1) \Rightarrow (f t1) | (pr0_comp u1 u2 p0 t1 t2 p1 k)
+\Rightarrow (f0 u1 u2 p0 ((pr0_ind P f f0 f1 f2 f3 f4 f5) u1 u2 p0) t1 t2 p1
+((pr0_ind P f f0 f1 f2 f3 f4 f5) t1 t2 p1) k) | (pr0_beta u v1 v2 p0 t1 t2
+p1) \Rightarrow (f1 u v1 v2 p0 ((pr0_ind P f f0 f1 f2 f3 f4 f5) v1 v2 p0) t1
+t2 p1 ((pr0_ind P f f0 f1 f2 f3 f4 f5) t1 t2 p1)) | (pr0_upsilon b n v1 v2 p0
+u1 u2 p1 t1 t2 p2) \Rightarrow (f2 b n v1 v2 p0 ((pr0_ind P f f0 f1 f2 f3 f4
+f5) v1 v2 p0) u1 u2 p1 ((pr0_ind P f f0 f1 f2 f3 f4 f5) u1 u2 p1) t1 t2 p2
+((pr0_ind P f f0 f1 f2 f3 f4 f5) t1 t2 p2)) | (pr0_delta u1 u2 p0 t1 t2 p1 w
+s0) \Rightarrow (f3 u1 u2 p0 ((pr0_ind P f f0 f1 f2 f3 f4 f5) u1 u2 p0) t1 t2
+p1 ((pr0_ind P f f0 f1 f2 f3 f4 f5) t1 t2 p1) w s0) | (pr0_zeta b n t1 t2 p0
+u) \Rightarrow (f4 b n t1 t2 p0 ((pr0_ind P f f0 f1 f2 f3 f4 f5) t1 t2 p0) u)
+| (pr0_tau t1 t2 p0 u) \Rightarrow (f5 t1 t2 p0 ((pr0_ind P f f0 f1 f2 f3 f4
+f5) t1 t2 p0) u)].