proposition: Lemma lexv_eq : forall n (xs ys : vector A n), lexv eq gt xs ys <-> (exists i (hi : i<n), gt (Vnth xs hi) (Vnth ys hi) /\ forall j, j<i -> forall hj : j<n, eq (Vnth xs hj) (Vnth ys hj)).
proof: Proof. intros n xs ys. unfold lexv. rewrite lexn_eq. split; intros [i [hi [h1 h2]]]; ex i hi; split. rewrite !projn_prod_of_vec in h1. hyp. intros j ji hj. gen (h2 _ ji hj). rewrite !projn_prod_of_vec. auto. rewrite !projn_prod_of_vec. hyp. intros j ji hj. rewrite !projn_prod_of_vec. fo. Qed.
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)