proposition: Lemma Ex_transportable3: ~ Transportableg \2c emptyset Ex_scheme2 (fun _ s => Vg s \0c = Vg s \1c).
proof: Proof. move: NS1 card1_nz NS2 card2_nz => qa qb qc qd. set x := slist2 (singleton \0c)(singleton \1c). set y := slist2 (singleton \0c)(singleton \0c). set s := slist2 \0c \1c. 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 \1c) => [sp1 sp2 sp3]. have hu: (slength Ex_scheme2) = \2c by rewrite /slength /Ex_scheme2; aw. set S1 := (slist1 (J \0c \1c)). set S2 := (slist1 (J \0c \2c)). move: (slist2_prop S1 S2); rewrite /= -/Ex_scheme2 => -[Sp1 Sp2 Sp3]. have snz: (slength S1 <> \0c)by rewrite /S1/slength/slist1; aw. have snz': (slength S2 <> \0c)by rewrite /S2/slength/slist1; aw. have cp2: (cpred \2c) = \1c by rewrite -(cpred_pr2 NS1) succ_one. have ha: Typificationg \2c emptyset Ex_scheme2 x s. split; [ exact:Ex_typ_aux2 | 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 cp2 xp3 sp3; fprops. have ax1: lf_axiom (fun z => \0c) (singleton \1c) (singleton \0c). by move => t _;fprops. have hb: Typ_hypg \2c x emptyset Ex_scheme2 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. + exact: ax1. + 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). have ra: inc \1c (domain Ex_scheme2) by rewrite /Ex_scheme2; aww. have rb: inc \0c (domain Ex_scheme2) by rewrite /Ex_scheme2; aww. rewrite /Typ_concg LgV// LgV//. rewrite (Typ_with_id_empty (proj1 fp1)) Sp2 Sp3 !echelon_trivial_extension //. rewrite /Vl cpred1 cp2 fp2 fp3 sp2 sp3 /f1 /f2 LfV // ? id_V //; fprops. bw; fprops;move => k;move/k: (erefl \0c);fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)