proposition: Lemma transport_unit E F g s x: bijection_prop g E F -> GT E s -> GL E s -> (inc x E /\ unit E s x) -> (inc (Vf g x) F /\ unit F (transport s g) (Vf g x)).
proof: Proof. move => Ha Hb Hc. have tsg:= (transport_op Ha Hb Hc). move:(Ha) => [[[fg gi] [_ gs]] sg tg]. rewrite sg in gi gs; rewrite tg in gs. move => [xE ux]; have yF: inc (Vf g x) F by Wtac. split => // z zF. move:(gs _ zF) => [z' zE ->]. by rewrite -(tsg _ _ xE zE)-(tsg _ _ zE xE); move: (ux _ zE) => [-> ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)