proposition: Lemma list_skipn_strong_ind : forall (A : Type) l (P : list A -> Prop) , P nil -> (forall x, (forall n, n > 0 -> P (skipn n x)) -> P x) -> P l.
proof: Proof. intuition. assert (l = skipn 0 l). simpl. trivial. rewrite H1. eapply list_skipn_strong_ind_h; trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia