Fix broken proofs for improved iFrame ∃

theories/lang/lib/arc.v

@@ -189,7 +189,7 @@ Section arc.
     iMod (own_alloc ((● (Some $ Cinl ((1/2)%Qp, xH, None), O) ⋅
                       ◯ (Some $ Cinl ((1/2)%Qp, xH, None), O))))
       as (γ) "[H● H◯]"; first by apply auth_both_valid_discrete.
-    iExists _, _. iFrame. iApply inv_alloc. iExists _. iFrame. iExists _. iFrame.
+    iFrame. iApply inv_alloc. iExists _. iFrame.
     rewrite Qp.div_2. auto.
   Qed.
 
@@ -314,7 +314,7 @@ Section arc.
       { by apply auth_update_alloc, prod_local_update_2,
               (op_local_update_discrete _ _ (1%nat)). }
       iMod ("Hclose1" with "[-Hown' HP HΦ]") as "_".
-      { iExists _. iFrame. iExists _.
+      { iExists _. iFrame.
         rewrite Z.add_comm -(Nat2Z.inj_add 1) /=. auto with iFrame. }
       iModIntro. wp_case. iApply "HΦ". iFrame.
     - destruct wlock.
@@ -407,7 +407,7 @@ Section arc.
             split; last by rewrite /= left_id; apply Hv. split=>[|//].
             apply frac_valid. rewrite /= -Heq comm_L.
             by apply Qp.add_le_mono_l, Qp.div_le. }
-          iFrame. iApply "Hclose1". iExists _. iFrame. iExists _. iFrame.
+          iFrame. iApply "Hclose1". iExists _. iFrame.
           rewrite /= [xH ⋅ _]comm_L frac_op [(_ + q')%Qp]comm -[(_ + _)%Qp]assoc
                   Qp.div_2 left_id_L. auto with iFrame.
         + iIntros "Hl". iFrame. iApply ("Hclose1" with "[-]"). iExists _. iFrame.
@@ -529,7 +529,7 @@ Section arc.
         iMod (own_update_2 _ _ _ _ with "H● Hown") as "H●".
         { apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_unit, _. }
         iMod ("Hclose" with "[- HΦ]") as "_".
-        { iExists _. iFrame. iExists (q + q'')%Qp. iCombine "HP1 HP1'" as "$".
+        { iExists _. iCombine "HP1 HP1'" as "HP". iFrame "H●". iFrame.
           iSplit; last by destruct s.
           iIntros "!> !%". rewrite assoc -Hq''. f_equal. apply comm, _. }
         iModIntro. wp_case. wp_op; case_bool_decide; simplify_eq. by iApply "HΦ".