proposition: Lemma trunc_trunc2 : forall (v : list A) (i j : nat), i <= j -> trunc (trunc v i) j = trunc v i.
proof: Proof. intros. rewrite (trunc_max (trunc v i) j). trivial with arith. apply le_trans with i. apply le_length_trunc. exact H. Qed.
imports: Arith_compl Minus Lists_compl