proposition: Lemma fmap_zip_with_l (g : C → A) l k : (∀ x y, g (f x y) = x) → length l ≤ length k → g <$> zip_with f l k = l.
proof: Proof. revert k. induction l; intros [|??] ??; f_equal/=; auto with lia. Qed.
imports: stdpp(options)