1 subgoal PROP : bi A : Type P : PROP Φ, Ψ : A → PROP ============================ "HP" : P "H" : ∃ a : A, Φ a ∨ Ψ a --------------------------------------∗ ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a 1 subgoal PROP : bi A : Type P : PROP Φ, Ψ : A → PROP x : A ============================ "HP" : P "H1" : Φ x --------------------------------------∗ ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a 1 subgoal PROP : bi A : Type P : PROP Φ, Ψ : A → PROP x : A ============================ "HP" : P "H2" : Ψ x --------------------------------------∗ ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a 1 subgoal PROP : bi A : Type P : PROP Φ, Ψ : A → PROP ============================ "HP" : P "H" : ∃ a : A, Φ a ∨ Ψ a --------------------------------------∗ ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a 1 subgoal PROP : bi A : Type P : PROP Φ, Ψ : A → PROP ============================ "H" : ∃ a : A, Φ a ∨ Ψ a --------------------------------------∗ ∃ x : A, Φ x ∨ Ψ x 1 subgoal PROP : bi A : Type P : PROP Φ, Ψ : A → PROP x : A ============================ "HP" : P "H1" : Φ x --------------------------------------∗ Φ x 1 subgoal PROP : bi A : Type P : PROP Φ, Ψ : A → PROP x : A ============================ "HP" : P "H2" : Ψ x --------------------------------------∗ P ∗ Ψ x 1 subgoal PROP : bi A : Type P : PROP Φ, Ψ : A → PROP ============================ "HP" : P --------------------------------------□ "H" : ∃ a : A, Φ a ∨ Ψ a --------------------------------------∗ ∃ a : A, Φ a ∨ P ∗ P ∗ Ψ a 1 subgoal PROP : bi A : Type P : PROP Φ, Ψ : A → PROP x : A ============================ "HP" : P --------------------------------------□ "H2" : Ψ x --------------------------------------∗ P ∗ P ∗ Ψ x 1 subgoal PROP : bi A : Type P, Q : PROP ============================ "HP" : P "HQ" : Q --------------------------------------□ □ (P ∗ Q) 1 subgoal I : biIndex PROP : bi Φ, Ψ : monPred I PROP ============================ "H1" : Φ "H2" : Φ -∗ Ψ --------------------------------------∗ Ψ 1 subgoal I : biIndex PROP : bi Φ, Ψ : monPred I PROP ============================ --------------------------------------∗ ∀ i : I, Φ i ∗ (Φ -∗ Ψ) i -∗ Ψ i 1 subgoal I : biIndex PROP : bi Φ : monPred I PROP P, Q : PROP ============================ "H2" : ⎡ P ⎤ --------------------------------------□ "H1" : ⎡ P -∗ Q ⎤ "H3" : Φ --------------------------------------∗ ⎡ P ∗ Q ⎤ 1 subgoal I : biIndex PROP : bi Φ : monPred I PROP P, Q : PROP ============================ "H2" : ⎡ P ⎤ --------------------------------------□ "H1" : ⎡ P -∗ Q ⎤ "H3" : Φ --------------------------------------∗ ⎡ Q ⎤