fact: Definition Vrel1_app n A (R : relation A) : relation (vector A n) := fun v1 v2 : vector A n => exists i (vi : vector A i) x j (vj : vector A j) h y, v1 = Vcast (Vapp vi (Vcons x vj)) h /\ v2 = Vcast (Vapp vi (Vcons y vj)) h /\ R x y.
imports: CoLoR(LogicUtil VecUtil RelUtil NatUtil SN)