intros p
case a
a : String
⊢ Sinf_const.eval (Sinf_const.coerce (O↗) (NoVars.S NoVars.O)) ≠ Sinf_const.eval (Sinf_const.coerce O NoVars.O)
case a
a : String
p : Sinf_const.eval (Sinf_const.coerce (O↗) (NoVars.S NoVars.O)) = Sinf_const.eval (Sinf_const.coerce O NoVars.O)
⊢ False