proposition: Lemma zip_with_inj `{!Inj2 (=) (=) (=) f} l1 l2 k1 k2 : length l1 = length k1 → length l2 = length k2 → zip_with f l1 k1 = zip_with f l2 k2 → l1 = l2 ∧ k1 = k2.
proof: Proof. rewrite <-!Forall2_same_length. intros Hl. revert l2 k2. induction Hl; intros ?? [] ?; f_equal; naive_solver. Qed.
imports: stdpp(options)