proposition: Lemma lexv_forall2_l : eq @ gt << gt -> Transitive eq -> forall n, Vforall2 eq (n:=n) @ lexv eq gt << lexv eq gt.
proof: Proof. intros gt_eq eq_trans n ts vs [us [tsus usvs]]. revert usvs. rewrite !lexv_eq. intros [i [hi [h1 h2]]]. ex i hi. split. apply gt_eq. exists (Vnth us hi). split. apply Vforall2_elim_nth. hyp. hyp. intros j ji jn. trans (Vnth us jn). apply Vforall2_elim_nth. hyp. fo. Qed.
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)