proposition: Lemma app_trunc_elemlist : forall (v : list A) (i : nat), S i <= length v -> trunc v i ++ elemlist v i = trunc v (S i).
proof: Proof. simple induction v. unfold elemlist in |- *. simpl in |- *. trivial with arith. simple induction i. simpl in |- *. unfold elemlist in |- *. rewrite trunc_O. rewrite strip_O. simpl in |- *. rewrite trunc_O. trivial with arith. intros. simpl in |- *. unfold elemlist in |- *. rewrite strip_cons_S. unfold elemlist in H. rewrite H. trivial with arith. generalize H1. simpl in |- *. auto with arith. Qed.
imports: Arith_compl Minus Lists_compl