proposition: Lemma nil_is_rht_unit: (is_rht_unit (app_as_csb_fun A) (empty_word A)).
proof: Proof. unfold is_rht_unit. simpl. intro x. induction x. simpl. intuition. 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