proposition: Lemma All_In_self {n} (v : vector A n) : All (fun x => In x v) v.
proof: Proof. induction v. constructor. constructor. constructor. eapply All_impl; eauto. simpl. intros. constructor; auto. Qed.
imports: Equations(Equations) Vector Sumbool