proposition: Theorem lexwf: forall l, NF l -> Acc LT l.
proof: Proof. induction l. - split; destruct 1 as [_ [H1 _]]. inversion H1. - split; split; intros; destruct a as [a n]. Abort. Lemma NF_inv1 : forall a n l, NF ((a,n)::l) -> NF l. Proof. destruct l. - constructor. - inversion_clear 1; assumption. Qed.
imports: Relations List Sorted Arith hydras(Restriction) Coq(Lia)