proposition: Lemma transportable_typification n A S: Typ_aux n A S -> Transportable n A S (Typification n A S).
proof: Proof. move => h; apply/transportable_casep1 => x s y f aux1. move: (aux1) (set1_1 \0c)=> [h2a h2b h2c h2d] i01. set S' := (Lg \1c (fun _ : Set => S)). have ls: slistp S' by rewrite /S';split; aw; fprops. have zds: inc \0c (domain S') by rewrite /S';aw. have ha: Typ_auxg n A S'. by move: h => [h1 h2 h3 h4];split => //; rewrite /S';aw => i li1; rewrite LgV. have hv: inc (Vg s \0c) (Typ_scheme x A S). move: h2a => [_ _ hu hv]; move: (proj2 hu); aw => sll; rewrite sll in hv. by move:(hv _ clt_01); rewrite /Typ_schemeg/S'; rewrite LgV. have slxn: slistpl x n by case: h2a. split => _ ; last by split. have zds': \0c <c domain S' by rewrite /S'; aw; apply:clt_01. have ww: (Typ_schemeg y A S' \0c) = (Typ_scheme y A S). rewrite /Typ_schemeg /Typ_scheme /S' LgV //. move:(@transportable_aux1 n x A S' s y f aux1) => [qa qb qc]; aw => qd. by move: (qd _ zds'); rewrite LgV//; rewrite ww; split. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)