proposition: Lemma Forall_nth d l : Forall P l ↔ ∀ i, i < length l → P (nth i l d).
proof: Proof. rewrite Forall_lookup. split. - intros Hl ? [x Hl']%lookup_lt_is_Some_2. rewrite (nth_lookup_Some _ _ _ _ Hl'). by eapply Hl. - intros Hl i x Hl'. specialize (Hl _ (lookup_lt_Some _ _ _ Hl')). by rewrite (nth_lookup_Some _ _ _ _ Hl') in Hl. Qed.
imports: stdpp(options)