proposition: Lemma Forall2_resize_r_flip l k x y n m : P x y → Forall (P x) k → length k = m → Forall2 P l (resize n y k) → Forall2 P (resize m x l) k.
proof: Proof. intros ?? <- ?. rewrite <-(resize_all k y) at 2. apply Forall2_resize_r with n; auto using Forall_true. Qed.
imports: stdpp(options)