Bug fix: Examples/ClosedProofs.lean and HeapLang/PrimitiveLaws.lean

Author: alvinylt

Iris/Iris/Examples/ClosedProofs.lean

@@ -63,7 +63,7 @@ example : True := by
   icases inv_alloc nroot ⊤ iprop(True) $$ [] with >#Hinv
   · itrivial
   imod inv_acc $$ Hinv with ⟨HP, Hcl⟩
-  · rw [nclose_root]; exact subset_refl
+  · rw [nclose_root]
   imod Hcl $$ HP with HP
   iapply fupd_mask_intro empty_subset
   iintro Hcl

Iris/Iris/HeapLang/PrimitiveLaws.lean

@@ -561,7 +561,8 @@ theorem wp_resolve_strong {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val ×
   · iapply HWPe; iexact Hp
   ihave HWPe := (show iprop(WP e @ s; E {{ v_e, ∃ pvs', proph p pvs' ∗
       ∀ pvs'', ⌜pvs' = (v_e, w) :: pvs''⌝ -∗ proph p pvs'' -∗ Φ v_e }}) ⊢ _
-    by rw [wp_unfold.to_eq]; simp only [wp.pre, hne]; exact .rfl) $$ HWPe
+    by rw [wp_unfold.to_eq]) $$ HWPe
+  simp only [wp.pre, hne]
   cases obs using List.reverseRec with
   | nil =>
     ihave Hσ_e : iprop(stateInterp σ₁ ns ([] ++ obs') nt) $$ [Hheap Hpmap]