Theorem: BunchImpl.BunchWithHole.sunit_eq (BunchImpl/Term/Bunch.lean)

State before:
P : Type u_1
b : Sort u_2
Γ : BunchWithHole P
⊢ sorryAx (X P b) true = Γ b ↔ sorryAx Prop true ∧ b = sorryAx (Sort u_2) true
Tactic:
rw [show (_ = _ ↔ _ = _) from ⟨Eq.symm, Eq.symm⟩]
State after:
P : Type u_1
b : Sort u_2
Γ : BunchWithHole P
⊢ Γ b = sorryAx (X P b) true ↔ sorryAx Prop true ∧ b = sorryAx (Sort u_2) true

State before:
P : Type u_1
b : Sort u_2
Γ : BunchWithHole P
⊢ Γ b = sorryAx (X P b) true ↔ sorryAx Prop true ∧ b = sorryAx (Sort u_2) true
Tactic:
simp
State after:
no goals