proposition: Lemma transportable_spec3 n A S R: (forall x s s', Typificationg n A S x s -> Typificationg n A S x s' -> (R x s <-> R x s')) -> Typ_auxg n A S -> (Transportableg n A S R <-> (forall x y, slistpl x n -> slistpl y n -> equipotent_fam n x y -> (forall u v, Typificationg n A S x u -> Typificationg n A S y v -> (R x u <-> R y v)))).
proof: Proof. move => h0 ts; move: (ts)=> [nN _ lS _]. split. move => TT x y [xl xs] [yl ys] eq1 s v hu hv. set f := Lg n (fun z => (equipotent_ex (Vg x z) (Vg y z))). have lf: slistpl f n. split; last by rewrite /slength /f;aw. by split; rewrite/f; fprops; aw. have fp: forall i, i <c n -> inc (Vg f i) (bijections (Vg x i) (Vg y i)). move => i lin; rewrite/f LgV//; last by apply/(NltP nN). by apply/bijectionsP/equipotent_ex_pr /card_eqP /eq1. have HA:(Typ_hypg n x A S s y f) by []. move: (transportable_aux1 HA) (TT _ _ _ _ HA) => sa sb. apply:(iff_trans sb); apply:(h0 _ _ _ sa hv). move => H x s y f [Ti ly lf hd]. have ra: slistpl x n by case: Ti. have rb: equipotent_fam n x y. by move => i /hd /bijectionsP bp; apply/card_eqP;exists (Vg f i). have rc: forall i, i <c slength S -> nonempty (Typ_schemeg x A S i). by move: Ti => [_ _ [_ ->]] h i /h hi; exists (Vg s i). apply: H => //. have /transportable_aux1 //: Typ_hypg n x A S s y f by []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)