proposition: Lemma list_remove_Permutation l1 l2 k1 x : l1 ≡ₚ l2 → list_remove x l1 = Some k1 → ∃ k2, list_remove x l2 = Some k2 ∧ k1 ≡ₚ k2.
proof: Proof. intros Hl. revert k1. induction Hl as [|y l1 l2 ? IH|y1 y2 l|l1 l2 l3 ? IH1 ? IH2]; simpl; intros k1 Hk1. - done. - case_decide; simplify_eq; eauto. destruct (list_remove x l1) as [l|] eqn:?; simplify_eq. destruct (IH l) as (?&?&?); simplify_option_eq; eauto. - simplify_option_eq; eauto using Permutation_swap. - destruct (IH1 k1) as (k2&?&?); trivial. destruct (IH2 k2) as (k3&?&?); trivial. exists k3. split; eauto. by trans k2. Qed.
imports: stdpp(options)