proposition: Lemma All_app {A P n m} (v : vector A n) (w : vector A m) : @All A P _ v -> All P w -> All P (app v w).
proof: Proof. funelim (app v w). auto. intros. depelim H0; simpl in *. constructor; auto. Qed.
imports: Equations(Equations) Vector