proposition: Lemma gt_WF : WF gt.
proof: Proof. Proof with auto; try contr. apply wf_transp_WF. intro x. destruct x... apply Acc_intro. intros. destruct y... Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)