proposition: Lemma behead_cons (T:Type) n (t : n.-tuple T) a : behead_tuple (cons_tuple a t) = t.
proof: Proof. rewrite /cons_tuple /behead_tuple /=. case: t => t tP /=. set X := (behead_tupleP _). by rewrite (eq_irrelevance X tP). Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)