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_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP ============================ "HP" : P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P ∗ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P --------------------------------------∗ True 1 subgoal PROP : sbi P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP ============================ _ : P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P ∗ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P --------------------------------------∗ True 1 subgoal PROP : sbi P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_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_P_P_P_P | P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }} --------------------------------------∗ True 1 subgoal PROP : sbi P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP ============================ _ : TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P | P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }} --------------------------------------∗ True 1 subgoal PROP : sbi P, Q : PROP Persistent0 : Persistent P Persistent1 : Persistent Q ============================ _ : P _ : Q --------------------------------------□ (P ∗ Q)