proposition: Lemma transport_p3 E F G s g h: GT E s -> bijection_prop g E F -> bijection_prop h F G-> transport (transport s g) h = transport s (h \co g).
proof: Proof. move => /setP_P sp [[[fg _] _] sg tg] [[[fh _] _] sh th]. have xop: h \coP g by split => //; ue. set_extens t. move/funI_P => [z /funI_P [u us ->] ->]; aw. move/setX_P: (sp _ us) => [pz /setX_P[pp pp1 pp2] qz]. apply/funI_P; ex_tac; rewrite !compfV //; ue. move => /funI_P [z zs ->]. move/setX_P: (sp _ zs) => [pz /setX_P[pp pp1 pp2] qz]. rewrite !compfV//; try ue; apply/funI_P. exists (J (J (Vf g (P (P z))) (Vf g (Q (P z)))) (Vf g (Q z))); aw; trivial. apply/funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)