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