proposition: Lemma comp_assoc' A (R S T : rel A) : R @ (S @ T) << (R @ S) @ T.
proof: Proof. unfold incl. intros. do 2 destruct H. do 2 destruct H0. exists x1; split. exists x0; split; hyp. exact H1. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)