proposition: Lemma clos_vaeq_union n R S : @clos_vaeq n (R U S) == @clos_vaeq n R U @clos_vaeq n S.
proof: Proof. unfold Def.clos_vaeq. rewrite Vrel1_union, comp_union_l, comp_union_r. refl. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)