proposition: Lemma codomE T U (f : T -> U) : codom f <--> \bigcup_x [set f x].
proof: Proof. by move=> y; split=> [[x fx]|[x [_ fx]]]; exists x. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)