proposition: Lemma sections_are_monic : Section' f → Monic f.
proof: Proof. autounfold. intros. destruct X0. rewrite <- c_left_id. symmetry. rewrite <- c_left_id. rewrite <- e. repeat (rewrite <- c_comp_assoc); try f_equal; auto. Qed.
imports: Hask.Prelude Hask.Crush Coq.Unicode.Utf8 FunctionalExtensionality