proposition: Lemma lexl_wf : WF lexl.
proof: Proof. assert (e : lexl << Rof (lexv (opt eq) (opt gt)) (vec_opt_of_list m)). intros x y xy. unfold Rof. rewrite lexv_eq. inversion xy; subst. ex i im. split. rewrite Vnth_vec_opt_of_list with (il:=ix), Vnth_vec_opt_of_list with (il:=iy). apply opt_intro. hyp. intros j ji jm. assert (jx : j < length x). lia. assert (jy : j < length y). lia. rewrite Vnth_vec_opt_of_list with (il:=jx), Vnth_vec_opt_of_list with (il:=jy). apply opt_intro. apply H0; hyp. rewrite e. apply WF_inverse. apply lexv_wf. apply wf_opt. hyp. class. apply opt_absorbs_left. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)