Theorem: BunchImpl.BunchWithHole.prop_eq (BunchImpl/Bunch.lean)

State before:
P : Sort u_1
φ : Typ P
b : Bunch P
Γ : BunchWithHole P
⊢ prop φ = ↑Γ b ↔ Γ = hole ∧ b = prop φ
Tactic:
rw [show (prop φ = _ ↔ _ = prop φ) from ⟨Eq.symm, Eq.symm⟩]
State after:
P : Sort u_1
φ : Typ P
b : Bunch P
Γ : BunchWithHole P
⊢ ↑Γ b = prop φ ↔ Γ = hole ∧ b = prop φ

State before:
P : Sort u_1
φ : Typ P
b : Bunch P
Γ : BunchWithHole P
⊢ ↑Γ b = prop φ ↔ Γ = hole ∧ b = prop φ
Tactic:
simp
State after:
no goals