proposition: Lemma transportable_GI: transportable (fun E s => ((GL E s /\ GA E s) /\ GU E s) /\ GI E s).
proof: Proof. move => E F s g bg typ. move: (proj1 (transportable_GT bg typ) typ) => typF. have rc:= (transportable_unit 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: ha ha' => [[lE aE] uE] [[lF aF] uF]. apply:(GE_prop13a typF lF uF aF) => x xF. move:(gs _ xF) => [y yE yv]. move:(GE_prop11l typ lE uE aE hb yE) => ll. move:(transport_inv bg typ lE uE yE ll) => hu. move:(GE_prop11r typ lE uE aE hb yE) => lr. have lr1: left_inverse E s (inverse E s y) y by case: lr. move:(transport_inv bg typ lE uE (proj1 ll) lr1) => hv1. have hv: right_inverse F (transport s g) (Vf g y) (Vf g (inverse E s y)) . move: hv1 => [rx ry]; split => //; exact: (proj1 hu). rewrite yv. by exists (Vf g (inverse E s y)). move: ha' ha => [[lE aE] uE] [[lF aF] uF]. apply:(GE_prop13a typ lE uE aE) => x xE. have xF: inc (Vf g x) F by Wtac. move : (GE_prop11l typF lF uF aF hb xF) (GE_prop11r typF lF uF aF hb xF). rewrite/left_inverse/right_inverse (transport_un bg typ lE uE). set y := inverse F _ _; move => [yF]. move:(gs _ yF)=> [z zE ->]. have st := (GE_prop2_stable typ lE). move:(st _ _ zE xE) (st _ _ xE zE) => h1f h2f. rewrite - (transport_op bg typ lE zE xE). rewrite - (transport_op bg typ lE xE zE) => e1 [_ e2]. have unE:= proj1(GE_prop7 typ lE uE). by exists z; split => //; split => //; apply: gi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)