proposition: Lemma Ex_transportable1: Transportableg \2c emptyset Ex_scheme1 (fun _ s => Vg s \0c = Vg s \1c).
proof: Proof. move => x s y f [ha hb hc hd]. move: NS1 card1_nz => ns1 c1nz. move: (slist2_prop (slist1 (J \0c \1c)) (slist1 (J \0c \1c))). move => [qa qb qc]. have hw: natp (slength Ex_scheme1) by rewrite/Ex_scheme1; aw; apply: NS2. have hu: inc \1c (domain Ex_scheme1) by rewrite /Ex_scheme1; aww. have hv: inc \0c (domain Ex_scheme1) by rewrite /Ex_scheme1; aww. have hv': \0c <c slength Ex_scheme1 by apply/(NltP). have hu': \1c <c slength Ex_scheme1 by apply/(NltP). rewrite /Typ_concg LgV// LgV//. rewrite (Typ_with_id_empty (proj1 hc)) qb qc echelon_trivial_extension //. rewrite /Vl cpred1; split => h; first by rewrite h. move: ha => [k1 k2 k3 k4]. rewrite (proj2 k3) in k4. move:(k4 _ hv') (k4 _ hu'). rewrite /Typ_schemeg qb qc echelon_trivial_value //. rewrite (slist_append_empty (proj1 k2)); Ytac w2; first by move/in_set0. rewrite /Vl cpred1 => ua ub. move: (hd _ (clt_02)) => /bijectionsP [[fa fb] fc fd]; apply:(proj2 fa). by rewrite fc. by rewrite fc. done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)