proposition: Theorem nth_error_app_length : forall (A : Set)(ls : list A) (a : A), nth_error (ls ++ (a :: nil)) (length ls) = Some a.
proof: Proof. induction ls; intuition; simpl in *. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation