\forall (c: C).(\forall (t: T).((nf2 c t) \to (sn3 c t)))
\def
\lambda (c: C).(\lambda (t: T).(\lambda (H: (nf2 c t)).(sn3_sing c t
\forall (c: C).(\forall (t: T).((nf2 c t) \to (sn3 c t)))
\def
\lambda (c: C).(\lambda (t: T).(\lambda (H: (nf2 c t)).(sn3_sing c t