proposition: Theorem Forall2_length : forall l l', Forall2 l l' -> length l = length l'.
proof: Proof. intros l. induction l as [|x l IH]; intros l' Hl'; inversion Hl'. - reflexivity. - cbn. f_equal. now apply IH. Qed.
imports: PeanoNat