proposition: Lemma elemlist_cons_S : forall (v : list A) (i : nat) (b : A), elemlist (b :: v) (S i) = elemlist v i.
proof: Proof. unfold elemlist in |- *. intros. rewrite strip_cons_S. trivial with arith. Qed.
imports: Arith_compl Minus Lists_compl