proposition: Lemma elem_of_zipped_map {A B} (f : list A → list A → A → B) l k x : x ∈ zipped_map f l k ↔ ∃ k' k'' y, k = k' ++ [y] ++ k'' ∧ x = f (reverse k' ++ l) k'' y.
proof: Proof. split. - revert l. induction k as [|z k IH]; simpl; intros l; inv 1. { by eexists [], k, z. } destruct (IH (z :: l)) as (k'&k''&y&->&->); [done |]. eexists (z :: k'), k'', y. by rewrite reverse_cons, <-(assoc_L (++)). - intros (k'&k''&y&->&->). revert l. induction k' as [|z k' IH]; [by left|]. intros l; right. by rewrite reverse_cons, <-!(assoc_L (++)). Qed.
imports: stdpp(options)