proposition: Theorem tl_skipn_eq : forall (A : Type)(ls : list A)(n : nat), tl (skipn n ls) = skipn (S n) ls.
proof: Proof. induction ls; intuition; simpl in *. rewrite skipn_nil. trivial. destruct n; simpl in *. trivial. eauto. Qed.
imports: FCF.FCF FCF.CompFold