proposition: Lemma imset0 T U (f : T -> U) : f @: set0 <--> set0.
proof: Proof. exact: bigcup_set0. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)