Fix exercises.

exercises/symbol_ghost.v

@@ -56,7 +56,7 @@ Section symbol_ghost.
   Lemma symbol_obs γ s n : counter γ n -∗ symbol γ s -∗ ⌜(s < n)%nat⌝.
   Proof.
     iIntros "Hc Hs".
-    iDestruct (own_valid_2 with "Hc Hs") as %[?%max_nat_included _]%auth_both_valid_discrete.
+    iCombine "Hc Hs" gives %[?%max_nat_included _]%auth_both_valid_discrete.
     iPureIntro. simpl in *. lia.
   Qed.
 End symbol_ghost.

exercises/two_state_ghost.v

@@ -54,7 +54,7 @@ Section two_state_ghost.
     two_state_auth γ b -∗ two_state_final γ -∗ ⌜b = true⌝.
   Proof.
     iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %[Hinc _]%auth_both_valid_discrete.
+    iCombine "H1 H2" gives %[Hinc _]%auth_both_valid_discrete.
     apply option_included in Hinc as [|([]&[]&_&?&_)];
       destruct b; naive_solver.
   Qed.