proposition: Lemma lexv_forall2_opt_r : gt @ eq << gt -> Transitive eq -> forall n, lexv (opt eq) (opt gt) @ Vforall2_opt (n:=n) eq << lexv (opt eq) (opt gt).
proof: Proof. intros gt_eq eq_trans n ts vs [us [tsus usvs]]. revert tsus. rewrite !lexv_eq. intros [i [hi [h1 h2]]]. ex i hi. destruct usvs as [k [k1 [k2 k3]]]. inversion h1; clear h1; subst. destruct (le_dec k i). exfalso. assert (a : i - k < n - k). lia. gen (Vforall2_elim_nth a k3). rewrite !Vnth_sub, Vnth_eq with (h2:=hi), Vnth_eq with (v:=vs) (h2:=hi), <- H0; try lia. intro e; inversion e; clear e; subst. fo. split. assert (a : i < k). lia. gen (Vforall2_elim_nth a k2). rewrite !Vnth_sub, Vnth_eq with (h2:=hi), Vnth_eq with (v:=vs) (h2:=hi), <- H0; auto. intro e; inversion e; clear e; subst. apply opt_intro. apply gt_eq. exists y. fo. intros j ji jn. gen (h2 _ ji jn). intro e; inversion e; clear e; subst. assert (a : j < k). lia. gen (Vforall2_elim_nth a k2). rewrite !Vnth_sub, Vnth_eq with (h2:=jn), Vnth_eq with (v:=vs) (h2:=jn), <- H3; auto. intro e; inversion e; clear e; subst. apply opt_intro. trans y0; hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)