proposition: Lemma list_map_app `{Equiv A} `{Equiv B} `{!Setoid_Morphism (f : A → B)} (l k : list A) : sfmap f (l & k) = sfmap f l & sfmap f k.
proof: Proof. pose proof (setoidmor_b f). now setoid_rewrite map_app. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads