proposition: Lemma Forall2_of_forall_nth : forall {IA:Inhab A} {IB:Inhab B} P r s, (forall n, n < length r -> P (nth n r) (nth n s)) -> length r = length s -> Forall2 P r s.
proof: Proof. Proof using. introv H E. gen s. induction r; intros; destruct s; tryfalse. { auto. } { rew_list in E. constructors. { applys H 0. rew_list. math. } { applys~ IHr. introv N. applys H (S n). rew_list. math. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)