proposition: Lemma app_assoc {d e f:nat} {A: Type} : forall (u: t A d)( v : t A e) (w: t A f), (u ++ v) ++ w == u ++ (v ++ w).
proof: Proof. intros. induction u; simpl. - reflexivity. - red. cbn; f_equal. apply IHu. Qed.
imports: Bool Arith Vector