Commit ddd73df1 authored by Robbert Krebbers's avatar Robbert Krebbers

Add lemma `fmap_map_seq`.

parent b3e550a1
Pipeline #24969 passed with stage
in 10 minutes and 17 seconds
......@@ -2131,6 +2131,14 @@ Section map_seq.
rewrite map_seq_app, map_seq_singleton.
by rewrite insert_union_singleton_r by (by rewrite map_seq_snoc_disjoint).
Qed.
Lemma fmap_map_seq {B} (f : A B) start xs :
f <$> map_seq start xs = map_seq start (f <$> xs).
Proof.
revert start. induction xs as [|x xs IH]; intros start; csimpl.
{ by rewrite fmap_empty. }
by rewrite fmap_insert, IH.
Qed.
End map_seq.
(** * Tactics *)
......
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