cases nv₁
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
nv₁ : NoVars (θ₁↗)
nv₂ : NoVars (θ₂↗)
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) nv₁) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) nv₂)
⊢ Δ ⋁ θ₁ =ₛ θ₂
case S
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
nv₂ : NoVars (θ₂↗)
a✝ : NoVars θ₁
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S a✝)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) nv₂)
⊢ Δ ⋁ θ₁ =ₛ θ₂