proposition: Lemma Vrel1_app_union n A (R S : relation A) : @Vrel1_app n _ (R U S) == @Vrel1_app n _ R U @Vrel1_app n _ S.
proof: Proof. rewrite rel_eq; intros v1 v2. split. intros [i [vi [x [j [vj [h [y [h1 [h2 [h3|h3]]]]]]]]]]. left. ex i vi x j vj h y. intuition. right. ex i vi x j vj h y. intuition. intros [h|h]; destruct h as [i [vi [x [j [vj [h [y [h1 [h2 h3]]]]]]]]]; ex i vi x j vj h y; intuition. Qed.
imports: CoLoR(LogicUtil VecUtil RelUtil NatUtil SN) Coq(Morphisms)