constructor <;> try constructor
case S_axiom
θ t✝ : Sinf_term
a✝ nv₁ nv₂ : NoVars t✝
e : Sinf_const.eval (Sinf_const.coerce t✝ nv₁) = Sinf_const.eval (Sinf_const.coerce t✝ nv₂)
⊢ Ø ⋁ t✝↗ =ₛ t✝↗
case S_axiom.nv₂.a
θ t✝ : Sinf_term
a✝ nv₁ nv₂ : NoVars t✝
e : Sinf_const.eval (Sinf_const.coerce t✝ nv₁) = Sinf_const.eval (Sinf_const.coerce t✝ nv₂)
⊢ NoVars t✝