proposition: Lemma Forall_impl A: forall (P Q : A -> Prop), (forall a, P a -> Q a) -> forall n (v : t A n), Forall P v -> Forall Q v.
proof: Proof. intros P Q H n v HPv. now induction HPv; constructor; [apply H|]. Qed.
imports: VectorDef PeanoNat Eqdep_dec