Theorem: formalFixed (Fine/SystemB/Theories.lean)

State before:
Γ : Ctx
⊢ formalTheory Γ → ▲Γ = Γ
Tactic:
intros h₁
State after:
Γ : Ctx
h₁ : formalTheory Γ
⊢ ▲Γ = Γ

State before:
Γ : Ctx
h₁ : formalTheory Γ
⊢ ▲Γ = Γ
Tactic:
funext
State after:
case h
Γ : Ctx
h₁ : formalTheory Γ
x✝ : Form
⊢ (▲Γ) x✝ = Γ x✝

State before:
Γ : Ctx
h₁ : formalTheory Γ
x : Form
⊢ (▲Γ) x = Γ x
Tactic:
ext
State after:
case a
Γ : Ctx
h₁ : formalTheory Γ
x : Form
⊢ (▲Γ) x ↔ Γ x

State before:
case a
Γ : Ctx
h₁ : formalTheory Γ
x : Form
⊢ (▲Γ) x ↔ Γ x
Tactic:
apply Iff.intro
State after:
case a.mp
Γ : Ctx
h₁ : formalTheory Γ
x : Form
⊢ (▲Γ) x → Γ x

case a.mpr
Γ : Ctx
h₁ : formalTheory Γ
x : Form
⊢ Γ x → (▲Γ) x