proposition: Lemma prefix_nat_r n a b (P: list_before (prefix_of_nat n) a b) (R: r b a) : False.
proof: Proof. destruct PO as [IRR T]. induction n; ins; rewrite filterP_app in *; ins; desf; rewrite ?app_nil_r; desf. all: repeat (rewrite list_before_app in *; desf; try (eby eapply list_before_nil); try (eby eapply list_before_singl); ins; desf); in_simp; try rewrite in_prefixes in *; eauto. all: try (rewrite ?in_app_iff in *; ins; desf; in_simp). all: try rewrite in_prefixes in *; eauto. all: try rewrite in_prefix_of_nat_iff in *; unfold clos_refl in *; desf; eauto 10. all: try (match goal with H: _ |- _ => eapply list_before_filterP_inv in H; [|by apply nodup_prefixes] end); eauto using prefixes_r. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt