proposition: Lemma transportable_aux1 n x A S s y f ( s' := Lg (domain S) (fun i => Vf (echelon_can_extension (Vg S i) (Typ_with_id f A)) (Vg s i))): Typ_hypg n x A S s y f -> Typificationg n A S y s'.
proof: Proof. move =>[[qa qb qc qd] hb hc hd]. set p := slength S; have qv := proj2 qc; rewrite qv in qd. have pN: natp p by rewrite /p;move : qc => [[ _ h] <-]. have ls': slistpl s' (slength S) by rewrite /s'; split; aw; split;aw; fprops. have eq2:= (proj2 qc). split => //; rewrite /s'; aw => i ils. have ids: inc i (domain S) by apply/(NltP pN). rewrite LgV//. move:(qd _ ils); rewrite /Typ_schemeg; Ytac w; first by move/in_set0. Ytac0. set G := (echelon_can_extension (Vg S i) (Typ_with_id f A)). suff: inc G (bijections (echelon_of_base (Vg S i) (slist_append x A)) (echelon_of_base (Vg S i) (slist_append y A)) ). by move /bijectionsP => [[[fg _] _] <- <-]; fprops. move:(qa) => [_ slA _ h]; move: (h _ ids) => [ec ecx]. by apply: (Typ_with_id_prop qb hb hc slA ec w ecx hd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)