Theorem: typeUniqueness (Nederpelt/STLC.lean)

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
σ τ : 𝕋 𝕍
⊢ (Γ ⊢ M : σ) → (Γ ⊢ M : τ) → σ = τ
Tactic:
intros h h'
State after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
σ τ : 𝕋 𝕍
h : Γ ⊢ M : σ
h' : Γ ⊢ M : τ
⊢ σ = τ

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
σ τ : 𝕋 𝕍
h : Γ ⊢ M : σ
h' : Γ ⊢ M : τ
⊢ σ = τ
Tactic:
unfold typingJudgement at *
State after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
σ τ : 𝕋 𝕍
h : typeOf Γ M = some σ
h' : typeOf Γ M = some τ
⊢ σ = τ

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
σ τ : 𝕋 𝕍
h : typeOf Γ M = some σ
h' : typeOf Γ M = some τ
⊢ σ = τ
Tactic:
rw [h, Option.some.injEq] at h'
State after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
σ τ : 𝕋 𝕍
h : typeOf Γ M = some σ
h' : σ = τ
⊢ σ = τ

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
σ τ : 𝕋 𝕍
h : typeOf Γ M = some σ
h' : σ = τ
⊢ σ = τ
Tactic:
assumption
State after:
no goals