proposition: Lemma transport_op E F g s: bijection_prop g E F -> GT E s -> GL E s -> forall a b, inc a E -> inc b E -> Vf g (VL s a b) = VL (transport s g) (Vf g a) (Vf g b).
proof: Proof. move => bg te law a b aE bE. move:(GE_prop2 te law) => law1. move/(transportable_GT bg te): (te) => typF. move/(transportable_GL bg te): law => lawF. move:(GE_prop2 typF lawF) => law2. apply: (Law_val law2); apply/funI_P. exists (J (J a b) (VL s a b)); [ by apply:(Law_in law1) | by aw ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)