proposition: Lemma transport_p2 E s: GT E s -> (transport s (identity E)) = s.
proof: Proof. move => /setP_P sp. set_extens t. move/funI_P => [z zs ->]. move/setX_P: (sp _ zs) => [pz /setX_P[pp pp1 pp2] qz]. by rewrite ! idV // pp pz. move => ts; move/setX_P: (sp _ ts) => [pz /setX_P[pp pp1 pp2] qz]. by apply/funI_P; ex_tac; rewrite ! idV // pp pz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)