proposition: Lemma Ex_transportable2: ~ Transportableg \2c emptyset Ex_scheme1 (fun x _ => Vg x \0c = Vg x \1c).
proof: Proof. move: NS1 card1_nz => qa qb. set x := slist2 (singleton \0c)(singleton \1c). set y := slist2 (singleton \0c)(singleton \0c). set s := slist2 \0c \0c. set f1 := identity (singleton \0c). set f2 := Lf (fun z => \0c) (singleton \1c)(singleton \0c). set f := slist2 f1 f2. move: (slist2_prop (singleton \0c)(singleton \1c)) => [xp1 xp2 xp3]. move: (slist2_prop (singleton \0c)(singleton \0c)) => [yp1 yp2 yp3]. move: (slist2_prop f1 f2) => [fp1 fp2 fp3]. move: (slist2_prop \0c \0c) => [sp1 sp2 sp3]. have hu: (slength Ex_scheme1) = \2c by rewrite /slength /Ex_scheme1; aw. set S := (slist1 (J \0c \1c)). move: (slist2_prop S S); rewrite /= -/Ex_scheme1 => -[Sp1 Sp2 Sp3]. have snz: (slength S <> \0c)by rewrite /S/slength/slist1; aw. have ha: Typificationg \2c emptyset Ex_scheme1 x s. split; [ exact:Ex_typ_aux1 | done | by rewrite hu | ]. rewrite /Typ_schemeg (slist_append_empty (proj1 xp1)) (proj2 sp1). move => i /clt2 [] ->; rewrite ?Sp2 ?Sp3 echelon_trivial_value//;Ytac0. - by rewrite /Vl cpred1 xp2 sp2; fprops. - by rewrite /Vl cpred1 xp2 sp3; fprops. have hb: Typ_hypg \2c x emptyset Ex_scheme1 s y f. split => //i /clt2 [] ->. - rewrite xp2 yp2 fp2/f1; apply/bijectionsP; saw; apply: identity_fb. - rewrite xp3 yp3 fp3 /f2;apply/bijectionsP; saw. apply:lf_bijective. + by move => t _;fprops. + by move => u v /set1_P -> /set1_P ->. + by move => u /set1_P ->; exists \1c; fprops. move => h; move:(h x s y f hb). rewrite /Typ_concg xp2 xp3 yp2 yp3 => bad. move/bad: (erefl (singleton \0c)) => /(f_equal (inc \0c)) hh. by move: (set1_1 \0c); rewrite hh => /set1_P e01; case:qb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)