proposition: Lemma empty_finType_code_set (C : code_set) : (#|T| = 0) -> C = [::] :> seq _ \/ C = [:: [::]] :> seq _.
proof: Proof. move=> T0. case/boolP : (C == [::] :> seq _); first by move/eqP; left. rewrite -size_eq0 => C0; right. have : size C <= 1. rewrite leqNgt. apply/negP => C2. have : exists a b, a \in C /\ b \in C /\ a != b. destruct C as [[|s1 [|s2 s3]] Hs] => //. simpl in *. exists s1, s2. rewrite !inE !eqxx /= orbT; split => //; split => //. apply/negP => /= /eqP s1s2. move: (Hs); by rewrite s1s2 !inE eqxx. case=> a; case=> b [aC [bC]]. apply/negP; by rewrite negbK (empty_finType_nil T0 a) (empty_finType_nil _ b). rewrite leq_eqVlt ltnS leqn0 (negbTE C0) orbF. destruct C as [s Hs] => /=. destruct s as [|s1 [|s2 s3]] => // _. by rewrite (empty_finType_nil T0 s1). Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext