proposition: Lemma strip_trunc_i : forall (v : list A) (i : nat), strip (trunc v i) i = nil.
proof: Proof. simple induction v. auto with arith. simple induction i. auto with arith. intros. simpl in |- *. rewrite strip_cons_S. apply H. Qed.
imports: Arith_compl Minus Lists_compl