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

State before:
P : Sort u_1
b Δ₁ Δ₂ : Bunch P
Γ : BunchWithHole P
⊢ ↑Γ b = (Δ₁ ;ᵇ Δ₂) ↔
    Γ = hole ∧ b = (Δ₁ ;ᵇ Δ₂) ∨ (∃ Γ', Γ = semiL Γ' Δ₂ ∧ ↑Γ' b = Δ₁) ∨ ∃ Γ', Γ = semiR Δ₁ Γ' ∧ ↑Γ' b = Δ₂
Tactic:
cases Γ <;> aesop
State after:
no goals