proposition: Lemma retractions_are_epic : Retraction f → Epic f.
proof: Proof. autounfold. intros. destruct X0. rewrite <- c_right_id. symmetry. rewrite <- c_right_id. rewrite <- e. repeat (rewrite c_comp_assoc); try f_equal; auto. Qed.
imports: Hask.Prelude Hask.Crush Coq.Unicode.Utf8 FunctionalExtensionality