diff --git a/theories/typing/lib/ghostcell.v b/theories/typing/lib/ghostcell.v index 6a5dc438303bc9c49774695bf2b01eede8088bc4..6ff1ae07f6566d2ca4e36fcf8d4cda3d0b670ce6 100644 --- a/theories/typing/lib/ghostcell.v +++ b/theories/typing/lib/ghostcell.v @@ -101,8 +101,8 @@ Section ghostcell. Proof. rewrite /Fractional=>q1 q2. rewrite -own_op /ghosttoken_st_to_R /=. f_equiv. - rewrite -Cinr_op. f_equiv. - rewrite -pair_op. f_equiv. + rewrite -Cinr_op. eapply Cinr_proper. + rewrite -pair_op. f_equiv; [|done..]. rewrite agree_idemp. done. Qed. diff --git a/theories/typing/own.v b/theories/typing/own.v index 20c253f3cf57f3665818ec763028b5d1907c6354..05911b2421258bd76c0c1d500923c6d64d778c51 100644 --- a/theories/typing/own.v +++ b/theories/typing/own.v @@ -39,7 +39,7 @@ Section own. - iSplit. + by iIntros "[[]?]". + by iIntros "[]". - - rewrite heap_freeable_op_eq. f_equiv. + - rewrite heap_freeable_op_eq. f_equiv; [|done..]. by rewrite -Qp_div_add_distr pos_to_Qp_add -Nat2Pos.inj_add. Qed.