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. destruct (qs l). simpl; eauto. destruct a. eapply (All_In _ _ H0). Qed.
imports: Equations(Equations) Vector Sumbool