proposition: Lemma gt0_wf : WF gt0.
proof: Proof. apply restrict_SN_clos_aeq_tc_supterm_acc_R_mon_wf; class. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil LCompSimple VecUtil RelUtil LCall LCompInt SetUtil SN NatUtil LCompRewrite EqUtil)