\forall (g: G).(\forall (a: A).(\forall (vs: TList).(\forall (c: C).(\forall
(i: nat).((arity g c (THeads (Flat Appl) vs (TLRef i)) a) \to ((nf2 c (TLRef
i)) \to ((sns3 c vs) \to (sc3 g a c (THeads (Flat Appl) vs (TLRef i))))))))))
\forall (g: G).(\forall (a: A).(\forall (vs: TList).(\forall (c: C).(\forall
(i: nat).((arity g c (THeads (Flat Appl) vs (TLRef i)) a) \to ((nf2 c (TLRef
i)) \to ((sns3 c vs) \to (sc3 g a c (THeads (Flat Appl) vs (TLRef i))))))))))