proposition: Lemma list_delete_subseteq i l : delete i l ⊆ l.
proof: Proof. revert i. induction l as [|x l IHl]; intros i; [done|]. destruct i as [|i]; [by apply list_subseteq_cons|by apply list_subseteq_skip]. Qed.
imports: stdpp(options)