1 subgoal PROP : sbi P, Q : PROP ============================ "H2" : ∀ x : nat, ⌜x = 0⌝ ∨ ⌜x = 1⌝ --------------------------------------□ "H" : □ (P ∨ Q) --------------------------------------∗ Q ∨ P 1 subgoal PROP : sbi P, Q : PROP ============================ "H2" : ∀ x : nat, ⌜x = 0⌝ ∨ ⌜x = 1⌝ _ : P --------------------------------------□ Q ∨ P 1 subgoal PROP : sbi P : PROP ============================ "HP" : (P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P) ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P --------------------------------------∗ P 1 subgoal PROP : sbi P : PROP ============================ _ : (P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P) ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P --------------------------------------∗ P 1 subgoal PROP : sbi P : PROP ============================ "HP" : TESTNOTATION {{ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P | P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P }} --------------------------------------∗ P 1 subgoal PROP : sbi P : PROP ============================ _ : TESTNOTATION {{ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P | P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P }} --------------------------------------∗ P 1 subgoal PROP : sbi P, Q : PROP Persistent0 : Persistent P Persistent1 : Persistent Q ============================ _ : P _ : Q --------------------------------------□ (P ∗ Q)