DEFINITION sc3_repl()
TYPE =
       ∀g:G.∀a1:A.∀c:C.∀t:T.(sc3 g a1 c t)→∀a2:A.(leq g a1 a2)→(sc3 g a2 c t)
BODY =
Show proof