proposition: Lemma transportable_casep1 n A S R (R' := fun x s => R x (Vg s \0c)): Transportable n A S R <-> Transportableg n A (Lg \1c (fun z => S)) R'.
proof: Proof. have i01: inc \0c \1c by apply: set1_1. have ww: inc \0c (domain (Lg \1c (fun _ : Set => S))) by aw. rewrite /Transportable /Transportableg; split. move => ha x s' y f [ [q1 q2 q3 q4] qb qc qd]. case: q1; case: q3; rewrite /slength Lgd => ua ub nN lA lsp lv. move:(lv _ i01); rewrite LgV// => - [es1 es2]. have: \0c <c slength s' by rewrite /slength ub; apply:clt_01. move/q4; rewrite /Typ_schemeg. rewrite LgV // => xx. by rewrite /Typ_concg /R' LgV // LgV //; apply: ha. move => ha x s y f [ [[q1a q1b q1c q1d] q2 q3] qb qc qd]. move:(ha x (Lg \1c (fun z => s)) y f). rewrite /Typ_concg /R'. rewrite (LgV i01) (LgV ww) (LgV i01) (LgV i01); apply. split => //; split. - split => //; rewrite /slistp; aw; fprops => i i1; rewrite LgV//. - done. - rewrite/slistpl /slistp; aw; split; fprops. - rewrite /Typ_schemeg /slength; aw; move => i /(NltP NS1) => i1. rewrite ! LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)