proposition: Lemma sat_init (Ns : n.-tuple (seq nat)) I : cat Ns I |= init <-> exists2 q, q \in nfa_s A & 0 \in tnth Ns (rank q).
proof: Proof. split. - move/sat_all1/(_ 0)/sat_imp. case/(_ _)/Wrap; first exact/sat_zero. case/sat_orE => s. rewrite mem_enum /= => B /sub1P C. exists s => //. by rewrite cat_prefix // -tnth_nth in C. - case => q q1 q2. apply/sat_all1 => m. rewrite sat_imp. move/sat_zero => /= B. have -> : m = 0. move: (B 0). by rewrite !inE eqxx => /eqP. apply (sat_orI (x := q)); first by rewrite mem_enum. apply/sub1P. by rewrite /= cat_prefix -?tnth_nth. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)