proposition: Lemma elemlist_cons_O : forall (v : list A) (b : A), elemlist (b :: v) 0 = b :: nil.
proof: Proof. intros. unfold elemlist in |- *. rewrite strip_O. simpl in |- *. rewrite trunc_O. trivial with arith. Qed.
imports: Arith_compl Minus Lists_compl