proposition: Theorem nth_option_some : forall (A : Set)(ls : list A) n, n < length ls -> exists a, nth_option ls n = Some a.
proof: Proof. induction ls; intuition; simpl in *. lia. destruct n. econstructor; eauto. destruct (IHls n). lia. econstructor; eauto. Qed.
imports: FCF.FCF