proposition: Lemma Forall_Nth_inv : forall P n l x, Forall P l -> Nth n l x -> P x.
proof: Proof. Proof using. introv F N. applys* Forall_mem_inv F. applys* Nth_mem. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)