proposition: Lemma gt_call_wf : (forall r, WF (gt_args r)) -> WF (gt_call gt_args).
proof: Proof. intro gt_args_wf. apply WF_inverse. apply wf_WF_transp. apply wf_lexprod. apply WF_wf_transp. apply gtC_wf. intro r. apply WF_wf_transp. apply gt_args_wf. Qed.
imports: Coq(Morphisms Basics Lexicographic_Product) CoLoR(LogicUtil LSimple VecUtil RelUtil VecOrd EqUtil Lexico SN NatUtil)