proposition: Lemma subrelation_proper `(mor : Proper A R' m) `(unc : Unconvertible (crelation A) R R') `(sub : subrelation A R' R) : Proper R m.
proof: Proof. intros. apply sub. apply mor. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Classes.CRelationClasses