proposition: Lemma morcls_eq_impl_morcls_cl_eq {C : category} {S T : morphism_class C} (HT : morphism_class_retract_closed T) : S = T -> S^cl = T.
proof: Proof. intro H. rewrite H. apply morphism_class_retract_closed_impl_eq_cl. exact HT. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.ModelCategories.Retract