proposition: Lemma imset_eq_ext a b (f g : a -> b) (A : set a) : (forall x, f x = g x) -> f @: A <--> g @: A.
proof: Proof. rewrite /imset /bigcup /set1. move => H x. split => [[i [H1 H2]] | [i [H1 H2]]]; eexists; split; try eassumption. congruence. congruence. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)