proposition: Lemma strip_cons_S : forall (v : list A) (i : nat) (b : A), strip (b :: v) (S i) = strip v i.
proof: Proof. unfold strip in |- *. simple induction i. simpl in |- *. elim minus_n_O. intro. replace (length v) with (length (rev A v)). rewrite trunc_all. rewrite trunc_app. rewrite trunc_all. elim minus_n_n. rewrite trunc_O. rewrite app_v_nil. trivial with arith. apply length_rev. intros. apply rev_eq. simpl in |- *. rewrite trunc_app. rewrite length_rev. rewrite minus_minus_lem1. rewrite trunc_O. rewrite app_v_nil. trivial with arith. Qed.
imports: Arith_compl Minus Lists_compl