proposition: Lemma transport_p1 E F s g: GT E s -> bijection_prop g E F -> GT F (transport s g).
proof: Proof. move => /setP_P sp [[[fg _] _] sg tg]. apply/setP_P => t /funI_P [z zs ->]. move/setX_P: (sp _ zs) => [pz /setX_P[pp pp1 pp2] qz]. apply:setXp_i; [ apply:setXp_i; Wtac | Wtac]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)