proposition: Lemma codom_const A B (x : B) : inhabited A -> codom (fun _ : A => x) <--> [set x].
proof: Proof. by move=> ?; rewrite codomE bigcup_const. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)