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

State before:
P : Type u_1
Γ Γ' : BunchWithHole P
φ φ' : Bunch P
⊢ Γ (sorryAx (Sort u_2) true) = Γ' (sorryAx (Sort u_2) true) →
    (∃ Δ, φ = ?m.12180131 Δ ∧ Γ.comp Δ = Γ') ∨
      (∃ Δ, φ' = ?m.12180132 Δ ∧ Γ'.comp Δ = Γ) ∨
        ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = Γ ∧ (Bunch P → Sort u_2 → sorryAx Prop true)
Tactic:
intro h
State after:
P : Type u_1
Γ Γ' : BunchWithHole P
φ φ' : Bunch P
h : Γ (sorryAx (Sort u_2) true) = Γ' (sorryAx (Sort u_2) true)
⊢ (∃ Δ, φ = ?m.12180131 Δ ∧ Γ.comp Δ = Γ') ∨
    (∃ Δ, φ' = ?m.12180132 Δ ∧ Γ'.comp Δ = Γ) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = Γ ∧ (Bunch P → Sort u_2 → sorryAx Prop true)