proposition: Lemma lt_wf : well_founded lt.
proof: Proof. destruct NA, NB; apply wf_disjoint_sum; [apply ON_wf | apply ON_wf0]. Qed.
imports: Coq(Arith Compare_dec Lia Relation_Operators RelationClasses Disjoint_Union) hydras(ON_Generic MoreOrders)