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