proposition: Lemma Ex_typ_aux1: Typ_auxg \2c emptyset Ex_scheme1.
proof: Proof. move:cle_12 slistp_0 NS2 => cle12 [ha hb] ns2; rewrite /Ex_scheme1. set S1 := (slist1 (J \0c \1c)). move: (slist2_prop S1 S1) => [[hc hd] he hf]. move: (echelon_trivial NS1 card1_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)