introv
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
⊢ ∀ {M M' : Λ V 𝕍} {Γ : TCtxt V 𝕍} {σ : 𝕋 𝕍}, (M =ₐ M') → (Γ ⊢ M : σ) → (Γ ⊢ M' : σ)
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M M' : Λ V 𝕍
Γ : TCtxt V 𝕍
σ : 𝕋 𝕍
⊢ (M =ₐ M') → (Γ ⊢ M : σ) → (Γ ⊢ M' : σ)