proposition: Lemma Forall2_nth_inv : forall {IA:Inhab A} {IB:Inhab B} P r s n, Forall2 P r s -> n < length r -> P (nth n r) (nth n s).
proof: Proof. Proof using. introv F N. forwards: Forall2_inv_length F. applys Forall2_Nth_inv n F; applys Nth_nth; math. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)