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