proposition: Lemma clos_vaeq_alt n : @clos_vaeq n R == @clos_vaeq n beta U @clos_vaeq n eta U @clos_vaeq n S.
proof: Proof. unfold Rh. rewrite !clos_mon_union, !clos_vaeq_union. refl. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(LogicUtil RelUtil VecOrd VecUtil LAlpha)