proposition: Lemma clos_aeq_union : forall R S, clos_aeq (R U S) == clos_aeq R U clos_aeq S.
proof: Proof. intros R S. split. induction 1. destruct H1 as [h|h]; [left|right]; (eapply clos_aeq_intro; [apply H | apply H0 | hyp]). intros t u [h|h]. eapply clos_aeq_incl. apply incl_union_l. refl. hyp. eapply clos_aeq_incl. apply incl_union_r. refl. hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)