proposition: Lemma delete_equiv_eq m1 m2 i : m1 ≡ delete i m2 ↔ ∃ m2', m1 = delete i m2' ∧ m2' ≡ m2.
proof: Proof. apply (partial_alter_equiv_eq _ _ _ _ _). intros ?? [=]%None_equiv_eq. Qed.
imports: Coq(Permutation) stdpp(options)