proposition: Lemma Vrel1_union n A (R S : relation A) : @Vrel1 n _ (R U S) == @Vrel1 n _ R U @Vrel1 n _ S.
proof: Proof. rewrite !Vrel1_app_eq. apply Vrel1_app_union. Qed.
imports: CoLoR(LogicUtil VecUtil RelUtil NatUtil SN) Coq(Morphisms)