proposition: Lemma search_infinite_R_wf xs : well_founded (R xs).
proof: Proof. revert xs. assert (help : ∀ xs n n', Acc (R (filter (.≠ f n') xs)) n → n' < n → Acc (R xs) n). { induction 1 as [n _ IH]. constructor; intros n2 [??]. apply IH; [|lia]. split; [done|]. apply elem_of_list_filter; naive_solver lia. } intros xs. induction (well_founded_ltof _ length xs) as [xs _ IH]. intros n1; constructor; intros n2 [Hn Hs]. apply help with (n2 - 1); [|lia]. apply IH. eapply filter_length_lt; eauto. Qed.
imports: stdpp(relations pretty) stdpp(options)