proposition: Lemma sfmap_id_applied `{Setoid A} (x : F A) : sfmap id x = x.
proof: Proof. change (sfmap id x = id x). apply setoids.ext_equiv_applied, sfmap_id. Qed.
imports: MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra MathClasses.interfaces.functors