proposition: Lemma to_word_strext: (fun_strext to_word_).
proof: Proof. unfold fun_strext; simpl. induction x; destruct y; firstorder with bool. Qed.
imports: Lia CoRN.algebra.CMonoids CoRN.model.monoids.Nmonoid CoRN.model.setoids.Nfinsetoid