proposition: Lemma Vrel1_lexv n A (gt : relation A) : Vrel1 (n:=n) gt << lexv Logic.eq gt.
proof: Proof. intros t u. rewrite Vrel1_nth_iff, lexv_eq. intros [i [hi [h1 h2]]]. ex i hi. firstorder auto with zarith. Qed.
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)