proposition: Lemma In_All {A P n} (v : vector A n) : All P v <-> (forall x, In x v -> P x).
proof: Proof. split. induction 1. intros. depelim H. auto. intros x; simpl. simp In. intuition. subst; auto. induction v; simpl; intros; auto; constructor. apply H; simp In; auto. firstorder. Qed.
imports: Equations(Equations) Vector