proposition: Lemma lexv_mon_arg A (eq gt : relation A) n (ts us : vector A n) p (ts' us' : vector A p) : lexv eq gt ts us -> lexv eq gt (Vapp ts ts') (Vapp us us').
proof: Proof. rewrite !lexv_eq. intros [i [i1 [i2 i3]]]. assert (hi : i < n + p). lia. ex i hi. split. rewrite !Vnth_app. destruct (le_gt_dec n i). lia. rewrite !Vnth_eq with (h1:=g) (h2:=i1); auto. intros j ji hj. rewrite !Vnth_app. destruct (le_gt_dec n j). lia. fo. Qed.
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)