proposition: Lemma qs_all {n} (l : vector A n) : forall x, In x (qs_forget l) -> In x l.
proof: Proof. intros x. unfold qs_forget. funelim (qs l); simpl. + trivial. + destruct qs_obligation_4. simpl. clear H1. intros Hx. apply In_app in Hx. destruct Hx. apply H in H1. destruct pr6. simpl in *. destruct a. destruct a. simpl in *. constructor. clear Heq. eapply All_In in a. intuition eauto. auto. clear Heq; intuition; destruct pr6; intuition; simpl in *. depelim H1. constructor. constructor. simpl in H1. apply H0 in H1. intuition. eapply All_In in H5. intuition eauto. auto. Qed.
imports: Equations(Equations) Vector Sumbool