proposition: Lemma zip_with_app_inv l k lC1 lC2 : zip_with f l k = lC1 ++ lC2 → ∃ l1 k1 l2 k2, lC1 = zip_with f l1 k1 ∧ lC2 = zip_with f l2 k2 ∧ l = l1 ++ l2 ∧ k = k1 ++ k2 ∧ length l1 = length k1.
proof: Proof. revert l k. induction lC1 as [|z lC1 IH]; simpl. { intros l k ?. by eexists [], [], l, k. } intros [|x l] [|y k] ?; simplify_eq/=. destruct (IH l k) as (l1&k1&l2&k2&->&->&->&->&?); [done |]. exists (x :: l1), (y :: k1), l2, k2; simpl; auto with congruence. Qed.
imports: stdpp(options)