proposition: Lemma list_skipn_strong_ind_h : forall (A : Type) l (P : list A -> Prop) , P nil -> (forall x, (forall n, n > 0 -> P (skipn n x)) -> P x) -> (forall n, P (skipn n l)).
proof: Proof. induction l; intuition; simpl in *. destruct n; simpl in *; trivial. destruct n; simpl in *. eapply H0. intuition. destruct n; try lia; simpl in *. eapply IHl; intuition. eapply IHl; intuition. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia