proposition: Lemma is_in_seq_not_Acc : forall x, is_in_seq x -> ~ Acc R x.
proof: Proof. intro x; pattern x; apply well_founded_ind with R; [assumption | ]. clear x; intros x IHx [i Hi]; subst x. specialize (IHx _ (decr_seq i)); destruct IHx. exists (S i);auto. apply Hwf. Qed.
imports: Relations List Sorted Arith hydras(Restriction) Coq(Lia)