proposition: Lemma zipped_Forall_app {A} (P : list A → list A → A → Prop) l k k' : zipped_Forall P l (k ++ k') → zipped_Forall P (reverse k ++ l) k'.
proof: Proof. revert l. induction k as [|x k IH]; simpl; [done |]. inv 1. rewrite reverse_cons, <-(assoc_L (++)). by apply IH. Qed.
imports: stdpp(options)