constructor <;> try assumption
case S.S
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S a✝¹)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) (NoVars.S a✝))
⊢ Δ ⋁ θ₁ =ₛ θ₂
case S.S.a
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S a✝¹)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) (NoVars.S a✝))
⊢ Sinf_const.eval (Sinf_const.coerce θ₁ a✝¹) = Sinf_const.eval (Sinf_const.coerce θ₂ a✝)