proposition: Lemma imset_id_ext T (A : set T) f : (forall x, f x = x) -> f @: A <--> A.
proof: Proof. rewrite /imset /bigcup => H x. split. - move => [y [H1 H2]]. rewrite H in H2. inversion H2. subst. assumption. - move => H1. eexists. split. eassumption. by rewrite H. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)