proposition: Lemma codom_subC (A : finType) (B : finType) (f : {ffun A -> B}) (p1 p2 : B) : (codom f \subset [:: p1; p2]) = (codom f \subset [:: p2; p1]).
proof: Proof. by apply/subsetP/subsetP; move => sB i /sB; rewrite !inE orbC. Qed.
imports: mathcomp(all_ssreflect finmap)