proposition: Lemma lookup_total_zip_with `{!Inhabited A, !Inhabited B, !Inhabited C} l k i : i < length l → i < length k → zip_with f l k !!! i = f (l !!! i) (k !!! i).
proof: Proof. intros [x Hx]%lookup_lt_is_Some_2 [y Hy]%lookup_lt_is_Some_2. by rewrite !list_lookup_total_alt, lookup_zip_with, Hx, Hy. Qed.
imports: stdpp(options)