proposition: Lemma Forall_nth l : Forall l <-> forall i d, i < length l -> P (nth i l d).
proof: Proof. split. - intros HF i d Hl. apply (Forall_forall l). + assumption. + apply nth_In; assumption. - intros HF. apply Forall_forall; intros a Hin. apply (In_nth _ _ a) in Hin; destruct Hin as [i [Hl Heq]]. rewrite <- Heq; intuition. Qed.
imports: PeanoNat