proposition: Lemma Forall2_resize l k x y n : P x y → Forall2 P l k → Forall2 P (resize n x l) (resize n y k).
proof: Proof. intros. rewrite !resize_spec, (Forall2_length l k) by done. auto using Forall2_app, Forall2_take, Forall2_replicate. Qed.
imports: stdpp(options)