proposition: Lemma Accs_all: forall a:A, Accs a.
proof: Proof. unfold Accs; intros a; pattern a; eapply well_founded_induction with (R:= ltA); [assumption|]; clear a ; intros a IHa. assert (Hl: forall n l, NF ((a,n)::l) -> Acc LT l). { destruct l. - intro; apply Acc_nil. - destruct p as [a0 n0]; intro H; apply IHa. + now inversion_clear H. + eapply NF_inv1; eauto. } intro n; pattern n; apply (well_founded_induction lt_wf). clear n; intros n Hn l H0. assert (H1: Acc LT l) by (eapply Hl; eauto); revert H0; pattern l; eapply Acc_ind with LT; [| eauto]; intros x0 H0 H2 H3. split; intros y H4. destruct (LT_inv H4) as [H5 | [H6 | [H7 | H8]]]. + subst; apply Acc_nil. + destruct H6 as [b [p [l'' [H6 H7]]]]; subst y. apply IHa; auto. now destruct H4. + destruct H7 as [l'' [H6 H7]]; subst. apply H2; auto. now destruct H4. + destruct H8 as [p [l'' [H6 H7]]]; subst; apply Hn; auto. now destruct H4. Qed.
imports: Relations List Sorted Arith hydras(Restriction) Coq(Lia)