proposition: Lemma transport_un E F g s: bijection_prop g E F -> GT E s -> GL E s -> GU E s -> un F (transport s g) = Vf g (un E s).
proof: Proof. move => bg ha hb hd. move: (GE_prop7 ha hb hd) => up. move:(transport_unit bg ha hb up) => [sa sb]. symmetry; apply: select_uniq => // a b aF ua bF ub . apply: (GE_prop6 aF ua bF ub). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)