proposition: Lemma imset_id T (A : set T) : id @: A <--> A.
proof: Proof. by move=> t; split=> [[x [Ax <-]]|At] //; exists t. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)