proposition: Lemma gt1_wf E : WF (gt1 E).
proof: Proof. apply gt_call_wf. apply gt_args_lex_wf. unfold gt. class. apply clos_aeq_tc_supterm_acc_wf. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil LCompSimple VecUtil RelUtil LCall LCompInt SetUtil SN NatUtil LCompRewrite EqUtil)