proposition: Lemma skipn_sum : forall (A : Type)(n2 n1 : nat)(ls : list A), skipn n1 (skipn n2 ls) = skipn (n2 + n1) ls.
proof: Proof. induction n2; intuition; simpl in *. destruct ls. destruct n1; trivial. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia