proposition: Lemma is_unit_Astar_empty_word: forall (A:CSetoid), (is_unit (Astar_as_CSemiGroup A)(empty_word A)).
proof: Proof. intro A. unfold is_unit. simpl. intro a. split. apply eq_fm_reflexive. unfold empty_word. induction a. apply eq_fm_reflexive. simpl. intuition. Qed.
imports: Coq.Arith.Euclid CoRN.model.Zmod.Cmod CoRN.algebra.CSemiGroups CoRN.tactics.csetoid_rewrite CoRN.model.structures.Nsec CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms