proposition: Lemma comp_clos_union R S : same (comp_clos (R U S)) (comp_clos R U comp_clos S).
proof: Proof. split. induction 1. destruct H1 as [h|h]; [left|right]; (eapply comp_clos_intro; [apply H | apply H0 | hyp]). intros t u [h|h]. eapply comp_clos_incl. apply incl_union_l. refl. hyp. eapply comp_clos_incl. apply incl_union_r. refl. hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)