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

State before:
P b : Type u_1
V : Bunch.X P b
Γ : BunchWithHole P
⊢ sorryAx ((fun x => Bunch.X P b) V) true = ↑(Γ b) V ↔
    sorryAx Prop true ∧ sorryAx (?m.4408005 Γ) true = sorryAx (?m.4408005 Γ) true
Tactic:
rw [eq_comm]
State after:
P b : Type u_1
V : Bunch.X P b
Γ : BunchWithHole P
⊢ ↑(Γ b) V = sorryAx ((fun x => Bunch.X P b) V) true ↔
    sorryAx Prop true ∧ sorryAx (?m.4408005 Γ) true = sorryAx (?m.4408005 Γ) true


⊢ {P b : Type u_1} → {V : Bunch.X P b} → BunchWithHole P → Sort u_2

State before:
P b : Type u_1
V : Bunch.X P b
Γ : BunchWithHole P
⊢ ↑(Γ b) V = sorryAx ((fun x => Bunch.X P b) V) true ↔
    sorryAx Prop true ∧ sorryAx (?m.4408005 Γ) true = sorryAx (?m.4408005 Γ) true


⊢ {P b : Type u_1} → {V : Bunch.X P b} → BunchWithHole P → Sort u_2
Tactic:
simp
State after:
P b : Type u_1
V : Bunch.X P b
Γ : BunchWithHole P
⊢ ↑(Γ b) V = sorryAx (Bunch.X P b) true ↔ sorryAx Prop true


⊢ {P b : Type u_1} → {V : Bunch.X P b} → BunchWithHole P → Sort u_2