proposition: Lemma Forall_nth_inv : forall {IA:Inhab A} P n l, Forall P l -> n < length l -> P (nth n l).
proof: Proof. Proof using. introv F N. applys Forall_Nth_inv n F. applys~ Nth_nth. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)