proposition: Lemma imset_comp T U V (f : U -> T) (g : V -> U) A : (f \o g) @: A <--> f @: (g @: A).
proof: Proof. by rewrite /imset bigcup_flatten; apply: eq_bigcupr => x; rewrite bigcup_set1. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)