proposition: Lemma sfmap_comp_applied `{Equiv A} `{Equiv B} `{Equiv C} `{!Setoid_Morphism (f : B → C)} `{!Setoid_Morphism (g : A → B)} (x : F A) : sfmap (f ∘ g) x = sfmap f (sfmap g x).
proof: Proof. change (sfmap (f ∘ g) x = (sfmap f ∘ sfmap g) x). pose proof (setoidmor_a g). apply setoids.ext_equiv_applied. now apply sfmap_comp. Qed.
imports: MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra MathClasses.interfaces.functors