proposition: Lemma Forall_forall A: forall P n (v : t A n), Forall P v <-> forall a, In a v -> P a.
proof: Proof. intros P n v. split. - intros H. induction H. + easy. + intros a [<-|?]%In_cons_iff; auto. - induction v as [|? ? v IHv]; intros Hin; constructor. + apply Hin; constructor. + apply IHv; intros a Ha. apply Hin; now constructor. Qed.
imports: VectorDef PeanoNat Eqdep_dec