proposition: Lemma range_is_substrate g: equivalence g -> range g = substrate g.
proof: Proof. move=> eg; rewrite /substrate; set_extens x. move => pa; fprops. move:(eg) => [fgg _ _ _]. case /setU2_P => //; move /(domainP (proj41 eg))=> [y Jg]. apply/(rangeP fgg); exists y; equiv_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)