proposition: Lemma Forall2_same_length {A B} (l : list A) (k : list B) : Forall2 (λ _ _, True) l k ↔ length l = length k.
proof: Proof. split; [by induction 1; f_equal/=|]. revert k. induction l; intros [|??] ?; simplify_eq/=; auto. Qed.
imports: stdpp(options)