proposition: Lemma imset_eq {T U} (A B : set T) (f : T -> U): A <--> B -> f @: A <--> f @: B.
proof: Proof. move => H u. split; apply imset_incl => t Ht; by apply H. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)