proposition: Lemma transportable_unit: transportable (fun E s => (GL E s /\ GA E s) /\ GU E s).
proof: Proof. move => E F s g bg typ. move: (proj1 (transportable_GT bg typ) typ) => typF. have rc:= (transportable_GA bg typ). move:(bg) => [[[fg gi] [_ gs]] sg tg]. rewrite sg in gi gs; rewrite tg in gs. split; move => [ha hb]; move/rc:(ha) => ha'; split => //. move:(GE_prop7 typ (proj1 ha) hb) => ra. move: (transport_unit bg typ (proj1 ha) ra) => [rb1 rb2]. exact:(GE_prop7_rev typF (proj1 ha') rb1 rb2). have ll := proj1 ha'. move:(GE_prop7 typF (proj1 ha) hb); set u := un _ _; move => [uF uu]. move:(gs _ uF) => [v vE vv]. have tsg:= (transport_op bg typ ll). apply:(GE_prop7_rev typ ll vE) => z zE. have zF: inc (Vf g z) F by Wtac. move: (uu _ zF); rewrite vv - !tsg //. by move => [ea eb]; split; apply: gi => //; apply: (GE_prop2_stable typ ll). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)