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