proposition: Lemma all2E s t : all2 s t = (size s == size t) && all [pred xy | r xy.1 xy.2] (zip s t).
proof: Proof. by elim: s t => [|x s IHs] [|y t] //=; rewrite IHs andbCA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)