proposition: Lemma Ex_typ_aux2: Typ_auxg \2c emptyset Ex_scheme2.
proof: Proof. move:(cleR CS2) cle_12 slistp_0 NS2 => c2 l2 [ha hb] ns2; rewrite /Ex_scheme1. set S1 := (slist1 (J \0c \1c)). set S2 := (slist1 (J \0c \2c)). move: (slist2_prop S1 S2) => [[hc hd] he hf]. move: (echelon_trivial NS1 card1_nz) => [p1 p2]. move: (echelon_trivial NS2 card2_nz) => [p1' p2']. split => //; rewrite [domain _]hd hb (csum0r CS2) => i /set2_P [] ->. by rewrite he p2. by rewrite hf p2'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)