proposition: Lemma Forall2_snd P l1 l2 k1 k2 : length l1 = length k1 → Forall2 P l2 k2 → Forall2 (λ x y, P (x.2) (y.2)) (zip l1 l2) (zip k1 k2).
proof: Proof. rewrite <-Forall2_same_length. intros Hlk1 Hlk2. revert l1 k1 Hlk1. induction Hlk2; intros ?? [|??????]; simpl; auto. Qed.
imports: stdpp(options)