proposition: Lemma trunc_trunc1 : forall (v : list A) (i : nat), trunc (trunc v i) i = trunc v i.
proof: Proof. simple induction v. simpl in |- *. trivial with arith. simple induction i. repeat rewrite trunc_O. trivial with arith. intros. simpl in |- *. rewrite H. trivial with arith. Qed.
imports: Arith_compl Minus Lists_compl