proposition: Lemma transportable_GA: transportable (fun E s => GL E s /\ GA E s).
proof: Proof. move => E F s g bg typ. have ra :=(transportable_GT bg typ). have rb :=(transportable_GL bg typ). move:(bg) => [[[fg gi] [_ gs]] sg tg]. rewrite sg in gi gs; rewrite tg in gs. move/ra:(typ) => typF. split; move => [ha hb]; move/rb: (ha) =>law2; split => //. move:(transport_op bg typ ha) => to. apply /(GE_prop4 typF law2) => a b c aF bF cF. move:(gs _ aF) (gs _ bF) (gs _ cF) => [a' aE av][b' bE bv][c' cE cv]. rewrite av bv cv. move:(GE_prop2_stable typ ha aE bE) => r1. move:(GE_prop2_stable typ ha bE cE) => r2. rewrite - (to _ _ bE cE) -(to _ _ aE bE). rewrite - (to _ _ aE r2) - (to _ _ r1 cE). by move/(GE_prop4 typ ha): hb => H; rewrite H. apply/(GE_prop4 typ law2) => a b c aE bE cE. move:(GE_prop2_stable typ law2 aE bE) => r1. move:(GE_prop2_stable typ law2 bE cE) => r2. move: (Vf_target fg); rewrite sg tg => H. move:(H _ aE) (H _ bE) (H _ cE) => aF bF cF. move /(GE_prop4 typF ha): hb => H'. move:(H' _ _ _ aF bF cF); clear H H'. move:(transport_op bg typ law2) => to. rewrite - (to _ _ bE cE) - (to _ _ aE r2) - (to _ _ aE bE) - (to _ _ r1 cE). by apply: gi; apply: (GE_prop2_stable typ law2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)