proposition: Lemma gt_red_wf R : WF (gt_red R).
proof: Proof. intros [f n ts]. apply SN_intro. intros [g p us] r. inv_gt_red r g p. gen (SN_inv h0 h). clear r h h0 ts. revert us; induction 1; rename x into ts. apply SN_intro. intros [g p us] r. inv_gt_red r g p. fo. Qed.
imports: Coq(Morphisms Basics Lexicographic_Product) CoLoR(LogicUtil LSimple VecUtil RelUtil VecOrd EqUtil Lexico SN NatUtil)