proposition: Lemma gt_WF : WF gt.
proof: Proof. apply wf_transp_WF. apply well_founded_lt_compat with (fun x => match x with | false => 0 | true => 1 end). destruct x; destruct y; unfold transp, gt; solve [tauto | auto with arith]. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)