proposition: Lemma Forall2_inserts l k l' k' i : Forall2 P l k → Forall2 P l' k' → Forall2 P (list_inserts i l' l) (list_inserts i k' k).
proof: Proof. intros ? H. revert i. induction H; eauto using Forall2_insert. Qed.
imports: stdpp(options)