proposition: Lemma gt_args_lex_wf : WF gt -> forall r, WF (gt_args_lex gt r).
proof: Proof. intros gt_wf r. apply WF_inverse. apply lexv_wf. apply wf_opt; hyp. class. apply opt_absorbs_left. intros t u [t' [tt' t'u]]. rewrite tt'. hyp. Qed.
imports: Coq(Morphisms Basics Lexicographic_Product) CoLoR(LogicUtil LSimple VecUtil RelUtil VecOrd EqUtil Lexico SN NatUtil)