fix metatheory

theories/heap_lang/metatheory.v

@@ -99,23 +99,23 @@ Lemma heap_closed_alloc σ l n w :
   map_Forall (λ _ v, is_closed_val v) (heap σ) →
   (∀ i : Z, 0 ≤ i → i < n → heap σ !! (l +ₗ i) = None) →
   map_Forall (λ _ v, is_closed_val v)
-             (heap σ ∪ heap_array l (replicate (Z.to_nat n) w)).
+             (heap_array l (replicate (Z.to_nat n) w) ∪ heap σ).
 Proof.
   intros Hn Hw Hσ Hl.
   eapply (map_Forall_ind
-            (λ k v, ((heap σ ∪ heap_array l (replicate (Z.to_nat n) w))
+            (λ k v, ((heap_array l (replicate (Z.to_nat n) w) ∪ heap σ)
                        !! k = Some v))).
   - apply map_Forall_empty.
   - intros m i x Hi Hix Hkwm Hm.
     apply map_Forall_insert_2; auto.
     apply lookup_union_Some in Hix; last first.
-    { symmetry; eapply heap_array_map_disjoint;
+    { eapply heap_array_map_disjoint;
         rewrite replicate_length Z2Nat.id; auto with lia. }
-    destruct Hix as [[j Hj]%elem_of_map_to_list%elem_of_list_lookup_1|
-                     (?&?&?&[-> Hlt%inj_lt]%lookup_replicate_1)%heap_array_lookup].
-    { apply map_Forall_to_list in Hσ.
-      by eapply Forall_lookup in Hσ; eauto; simpl in *. }
-    rewrite !Z2Nat.id in Hlt; eauto with lia.
+    destruct Hix as [(?&?&?&[-> Hlt%inj_lt]%lookup_replicate_1)%heap_array_lookup|
+                     [j Hj]%elem_of_map_to_list%elem_of_list_lookup_1].
+    + rewrite !Z2Nat.id in Hlt; eauto with lia.
+    + apply map_Forall_to_list in Hσ.
+      by eapply Forall_lookup in Hσ; eauto; simpl in *.
   - apply map_Forall_to_list, Forall_forall.
     intros [? ?]; apply elem_of_map_to_list.
 Qed.