proposition: Lemma gt_Fin_WF x : Acc (transp gt) (TPos x).
proof: Proof. induction x using lt_wf_ind; apply Acc_intro; destruct y; auto || contr. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)