-let rec wf3_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (m: nat).(P
-(CSort m) (CSort m)))) (f0: (\forall (c1: C).(\forall (c2: C).((wf3 g c1 c2)
-\to ((P c1 c2) \to (\forall (u: T).(\forall (t: T).((ty3 g c1 u t) \to
+implied rec lemma wf3_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (m:
+nat).(P (CSort m) (CSort m)))) (f0: (\forall (c1: C).(\forall (c2: C).((wf3 g
+c1 c2) \to ((P c1 c2) \to (\forall (u: T).(\forall (t: T).((ty3 g c1 u t) \to