proposition: Lemma transportable_spec_p0 n A S R: slength S = \0c -> Typ_auxg n A S -> (Transportableg n A S R <-> (forall x y, slistpl x n -> slistpl y n -> equipotent_fam n x y -> (R x emptyset <-> R y emptyset))).
proof: Proof. move => h1 ts; move: (ts)=> [nN _ lS _]. split. move => TT x y [xl xs] [yl ys] eq. 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. split; rewrite/f; aww; by exists n. have s0:domain emptyset = \0c by rewrite domain_set0. have le: slistpl emptyset (slength S). rewrite h1; split =>//;split;try apply:fgraph_set0. by rewrite s0;apply:NS0. have ha: Typificationg n A S x emptyset. by split => // i; rewrite /slength s0 => /clt0. have hb: Typ_hypg n x A S emptyset y f. split => // i lin; move/ (NltP nN): (lin) => lin1. apply/bijectionsP; rewrite /f LgV//; apply: equipotent_ex_pr. by apply/card_eqP; apply: eq. move:(TT x emptyset y f hb); rewrite /Typ_concg (slist_emptyp lS h1). by rewrite domain_set0 /Lg funI_set0. move => Hxy x s y f [ha hb hc hd]. rewrite /Typ_concg (slist_emptyp lS h1) domain_set0 /Lg funI_set0. move:ha => [_ he ls _]; rewrite h1 in ls. rewrite (slist_emptyp (proj1 ls) (proj2 ls)); apply: Hxy => //. by move => i /hd /bijectionsP bp; apply /card_eqP; exists (Vg f i). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)