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