proposition: Lemma Forall2_unique l k1 k2 : Forall2 P l k1 → Forall2 P l k2 → (∀ x y1 y2, P x y1 → P x y2 → y1 = y2) → k1 = k2.
proof: Proof. intros H. revert k2. induction H; inv 1; intros; f_equal; eauto. Qed.
imports: stdpp(options)