From 52431749b2df3cfd28dca8b6083d2d718f71a940 Mon Sep 17 00:00:00 2001 From: Kimaya Bedarkar <kbedarka@mpi-sws.org> Date: Wed, 12 Feb 2025 10:20:17 +0100 Subject: [PATCH] add new line back --- stdpp/list.v | 1 + 1 file changed, 1 insertion(+) diff --git a/stdpp/list.v b/stdpp/list.v index bd2b29d1..a29f6ecf 100644 --- a/stdpp/list.v +++ b/stdpp/list.v @@ -5039,6 +5039,7 @@ Section zip. rewrite <-Forall2_same_length. intros Hlk1 Hlk2. revert l1 k1 Hlk1. induction Hlk2; intros ?? [|??????]; simpl; auto. Qed. + Lemma elem_of_zip_l x1 x2 l k : (x1, x2) ∈ zip l k → x1 ∈ l. Proof. intros ?%elem_of_zip_with. naive_solver. Qed. -- GitLab