Theorem: BunchImpl.Equiv.hole_prop_inv (BunchImpl/Equiv.lean)

State before:
P : Type u_1
Γ : BunchWithHole P
A : Typ P
Δ : Bunch P
⊢ ↑Γ (prop A) ≈ Δ → ∃ Γ', Δ = ↑Γ' (prop A)
Tactic:
intro e
State after:
P : Type u_1
Γ : BunchWithHole P
A : Typ P
Δ : Bunch P
e : ↑Γ (prop A) ≈ Δ
⊢ ∃ Γ', Δ = ↑Γ' (prop A)

State before:
P : Type u_1
Γ : BunchWithHole P
A : Typ P
Δ : Bunch P
e : ↑Γ (prop A) ≈ Δ
⊢ ∃ Γ', Δ = ↑Γ' (prop A)
Tactic:
induction Δ
State after:
case prop
P : Type u_1
Γ : BunchWithHole P
A a✝ : Typ P
e : ↑Γ (prop A) ≈ prop a✝
⊢ ∃ Γ', prop a✝ = ↑Γ' (prop A)

case cunit
P : Type u_1
Γ : BunchWithHole P
A : Typ P
e : ↑Γ (prop A) ≈ cunit
⊢ ∃ Γ', cunit = ↑Γ' (prop A)

case comma
P : Type u_1
Γ : BunchWithHole P
A : Typ P
a✝¹ a✝ : Bunch P
a_ih✝¹ : ↑Γ (prop A) ≈ a✝¹ → ∃ Γ', a✝¹ = ↑Γ' (prop A)
a_ih✝ : ↑Γ (prop A) ≈ a✝ → ∃ Γ', a✝ = ↑Γ' (prop A)
e : ↑Γ (prop A) ≈ (a✝¹ ,ᵇ a✝)
⊢ ∃ Γ', (a✝¹ ,ᵇ a✝) = ↑Γ' (prop A)

case sunit
P : Type u_1
Γ : BunchWithHole P
A : Typ P
e : ↑Γ (prop A) ≈ sunit
⊢ ∃ Γ', sunit = ↑Γ' (prop A)

case semi
P : Type u_1
Γ : BunchWithHole P
A : Typ P
a✝¹ a✝ : Bunch P
a_ih✝¹ : ↑Γ (prop A) ≈ a✝¹ → ∃ Γ', a✝¹ = ↑Γ' (prop A)
a_ih✝ : ↑Γ (prop A) ≈ a✝ → ∃ Γ', a✝ = ↑Γ' (prop A)
e : ↑Γ (prop A) ≈ (a✝¹ ;ᵇ a✝)
⊢ ∃ Γ', (a✝¹ ;ᵇ a✝) = ↑Γ' (prop A)

State before:
P : Type u_1
Γ : BunchWithHole P
A a✝ : Typ P
e : ↑Γ (prop A) ≈ prop a✝
⊢ ∃ Γ', prop a✝ = ↑Γ' (prop A)
Tactic:
case prop =>
  simp at e
  refine ⟨.hole,?_⟩; simp
State after:
P : Type u_1
Γ : BunchWithHole P
A a✝ : Typ P
e : ↑Γ (prop A) ≈ prop a✝
⊢ a✝ = A

State before:
case cunit
P : Type u_1
Γ : BunchWithHole P
A : Typ P
e : ↑Γ (prop A) ≈ cunit
⊢ ∃ Γ', cunit = ↑Γ' (prop A)

case comma
P : Type u_1
Γ : BunchWithHole P
A : Typ P
a✝¹ a✝ : Bunch P
a_ih✝¹ : ↑Γ (prop A) ≈ a✝¹ → ∃ Γ', a✝¹ = ↑Γ' (prop A)
a_ih✝ : ↑Γ (prop A) ≈ a✝ → ∃ Γ', a✝ = ↑Γ' (prop A)
e : ↑Γ (prop A) ≈ (a✝¹ ,ᵇ a✝)
⊢ ∃ Γ', (a✝¹ ,ᵇ a✝) = ↑Γ' (prop A)

case sunit
P : Type u_1
Γ : BunchWithHole P
A : Typ P
e : ↑Γ (prop A) ≈ sunit
⊢ ∃ Γ', sunit = ↑Γ' (prop A)

case semi
P : Type u_1
Γ : BunchWithHole P
A : Typ P
a✝¹ a✝ : Bunch P
a_ih✝¹ : ↑Γ (prop A) ≈ a✝¹ → ∃ Γ', a✝¹ = ↑Γ' (prop A)
a_ih✝ : ↑Γ (prop A) ≈ a✝ → ∃ Γ', a✝ = ↑Γ' (prop A)
e : ↑Γ (prop A) ≈ (a✝¹ ;ᵇ a✝)
⊢ ∃ Γ', (a✝¹ ;ᵇ a✝) = ↑Γ' (prop A)
Tactic:
sorry
State after:
case comma
P : Type u_1
Γ : BunchWithHole P
A : Typ P
a✝¹ a✝ : Bunch P
a_ih✝¹ : ↑Γ (prop A) ≈ a✝¹ → ∃ Γ', a✝¹ = ↑Γ' (prop A)
a_ih✝ : ↑Γ (prop A) ≈ a✝ → ∃ Γ', a✝ = ↑Γ' (prop A)
e : ↑Γ (prop A) ≈ (a✝¹ ,ᵇ a✝)
⊢ ∃ Γ', (a✝¹ ,ᵇ a✝) = ↑Γ' (prop A)

case sunit
P : Type u_1
Γ : BunchWithHole P
A : Typ P
e : ↑Γ (prop A) ≈ sunit
⊢ ∃ Γ', sunit = ↑Γ' (prop A)

case semi
P : Type u_1
Γ : BunchWithHole P
A : Typ P
a✝¹ a✝ : Bunch P
a_ih✝¹ : ↑Γ (prop A) ≈ a✝¹ → ∃ Γ', a✝¹ = ↑Γ' (prop A)
a_ih✝ : ↑Γ (prop A) ≈ a✝ → ∃ Γ', a✝ = ↑Γ' (prop A)
e : ↑Γ (prop A) ≈ (a✝¹ ;ᵇ a✝)
⊢ ∃ Γ', (a✝¹ ;ᵇ a✝) = ↑Γ' (prop A)

State before:
P : Type u_1
Γ : BunchWithHole P
A a✝ : Typ P
e : ↑Γ (prop A) ≈ prop a✝
⊢ ∃ Γ', prop a✝ = ↑Γ' (prop A)
Tactic:
refine ⟨.hole,?_⟩
State after:
P : Type u_1
Γ : BunchWithHole P
A a✝ : Typ P
e : ↑Γ (prop A) ≈ prop a✝
⊢ prop a✝ = ↑BunchWithHole.hole (prop A)

State before:
P : Type u_1
Γ : BunchWithHole P
A a✝ : Typ P
e : ↑Γ (prop A) ≈ prop a✝
⊢ prop a✝ = ↑BunchWithHole.hole (prop A)
Tactic:
simp
State after:
P : Type u_1
Γ : BunchWithHole P
A a✝ : Typ P
e : ↑Γ (prop A) ≈ prop a✝
⊢ a✝ = A