proposition: Lemma Ord_wf : well_founded (transp gtA).
proof: Proof. apply well_founded_lt_compat with (f := fun x => match x with a => 1 | _ => 0 end). destruct x; destruct y; try_solve. Qed.
imports: CoLoR(TermsSig Horpo HorpoWf RelExtras Terms LogicUtil) Coq(Wf_nat List)