proposition: Theorem skipn_length : forall (A : Set) n0 (ls : list A), length (skipn n0 ls) = (length ls) - n0.
proof: Proof. induction n0; intuition; simpl in *. destruct ls; simpl. trivial. eauto. Qed.
imports: FCF.FCF FCF.SemEquiv