fact: Definition rel2_on_vec X (R : X -> X -> Prop) (v : vec X 2) : Prop := R (vec_head v) (vec_head (vec_tail v)).
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations)