proposition: Lemma app_v_trunc : forall (v1 v2 : list A) (i : nat), v1 ++ trunc v2 i = trunc (v1 ++ v2) (length v1 + i).
proof: Proof. intros. rewrite trunc_app. rewrite (trunc_max v1 (length v1 + i)). replace (length v1 + i - length v1) with i. trivial with arith. auto with arith. auto with arith. Qed.
imports: Arith_compl Minus Lists_compl