Commit 6401d876 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix inconsistent space.

parent 9bd10869
...@@ -3470,7 +3470,7 @@ Section fmap. ...@@ -3470,7 +3470,7 @@ Section fmap.
- exists y. split; [done | by left]. - exists y. split; [done | by left].
- destruct IH as [z [??]]. done. exists z. split; [done | by right]. - destruct IH as [z [??]]. done. exists z. split; [done | by right].
Qed. Qed.
Lemma elem_of_list_fmap l x : x ∈ f <$> l ↔ ∃ y, x = f y ∧ y ∈ l. Lemma elem_of_list_fmap l x : x ∈ f <$> l ↔ ∃ y, x = f y ∧ y ∈ l.
Proof. Proof.
naive_solver eauto using elem_of_list_fmap_1_alt, elem_of_list_fmap_2. naive_solver eauto using elem_of_list_fmap_1_alt, elem_of_list_fmap_2.
Qed. Qed.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment