proposition: Lemma Sorted_app {A R n m} (v : vector A n) (w : vector A m) : @Sorted A R _ v -> Sorted R w -> Sorted R (app v w).
proof: Proof. Admitted. Lemma In_app {A n m} (v : vector A n) (w : vector A m) (a : A) : In a v \/ In a w <-> In a (app v w). Proof. funelim (app v w). intuition. depelim H0. split. intros; depelim H0; simp In in *; intuition. simp In in *. intuition. apply H in H1. intuition. Qed.
imports: Equations(Equations) Vector