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