proposition: Theorem nth_error_app_Some : forall (A : Set)(ls : list A) n (a a' : A), nth_error ls n = Some a -> nth_error (ls ++ (a' :: nil)) n = Some a.
proof: Proof. induction ls; destruct n; intuition; simpl in *. inversion H. inversion H. eapply IHls. trivial. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation