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

State before:
P : Sort u_1
b : Bunch P
φ : Typ P
Γ : BunchWithHole P
⊢ ↑Γ b = prop φ ↔ Γ = hole ∧ b = prop φ
Tactic:
cases Γ <;> simp [FunLike.coe, subst]
State after:
no goals