-let rec sn3_ind (c: C) (P: (T \to Prop)) (f: (\forall (t1: T).(((\forall (t2:
-T).((((eq T t1 t2) \to (\forall (P0: Prop).P0))) \to ((pr3 c t1 t2) \to (sn3
-c t2))))) \to (((\forall (t2: T).((((eq T t1 t2) \to (\forall (P0:
-Prop).P0))) \to ((pr3 c t1 t2) \to (P t2))))) \to (P t1))))) (t: T) (s0: sn3
-c t) on s0: P t \def match s0 with [(sn3_sing t1 s1) \Rightarrow (f t1 s1
-(\lambda (t2: T).(\lambda (p: (((eq T t1 t2) \to (\forall (P0:
-Prop).P0)))).(\lambda (p0: (pr3 c t1 t2)).((sn3_ind c P f) t2 (s1 t2 p
-p0))))))].
+implied rec lemma sn3_ind (c: C) (P: (T \to Prop)) (f: (\forall (t1:
+T).(((\forall (t2: T).((((eq T t1 t2) \to (\forall (P0: Prop).P0))) \to ((pr3
+c t1 t2) \to (sn3 c t2))))) \to (((\forall (t2: T).((((eq T t1 t2) \to
+(\forall (P0: Prop).P0))) \to ((pr3 c t1 t2) \to (P t2))))) \to (P t1)))))
+(t: T) (s0: sn3 c t) on s0: P t \def match s0 with [(sn3_sing t1 s1)
+\Rightarrow (f t1 s1 (\lambda (t2: T).(\lambda (p: (((eq T t1 t2) \to
+(\forall (P0: Prop).P0)))).(\lambda (p0: (pr3 c t1 t2)).((sn3_ind c P f) t2
+(s1 t2 p p0))))))].