simp
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M M' : Λ V 𝕍
Γ : TCtxt V 𝕍
σ : 𝕋 𝕍
h : M =ₐ M'
h' : Γ ⊢ M : σ
x : V
⊢ none = none ∧ getType x Γ = getType x Γ ∨ ∃ y, none = some y ∧ getType x Γ = getType y Γ
no goals