proposition: Lemma sat_exn n s I : (I |= exn n s) <-> (exists Ns : n.-tuple (seq nat), cat Ns I |= s).
proof: Proof. elim: n I => [|n IH] I. - split. + exists [tuple]. rewrite /cat /=. apply: weak_coincidence H => X. by rewrite subn0. + case => Ns. rewrite tuple0 /cat /=. apply: weak_coincidence => X. by rewrite subn0. - have agr Ns N X : cat (rcons Ns N) I X =i cat Ns (cons N I) X. { rewrite /cat /= !size_rcons ltnS. case: (ltngtP X (size Ns)) => B. * by rewrite ?(ltnW B) nth_rcons B. * try rewrite leqNgt B /=. by rewrite -[X - size Ns]prednK ?subn_gt0 //= subnS. * by rewrite ?B ?leqnn ?subnn nth_rcons ltnn eqxx. } rewrite /=. split => [[N] /IH [Ns A]|]. + exists [tuple of rcons Ns N]. apply: weak_coincidence A => X k. by rewrite agr. + case. case => Ns /=. elim/last_ind : Ns => // Ns N _. rewrite size_rcons eqSS => A B. exists N. apply/IH. exists (Tuple A) => /=. exact: weak_coincidence _ B. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)