proposition: Lemma Forall_cons_iff A: forall (P : A -> Prop) a n (v : t A n), Forall P (a :: v) <-> P a /\ Forall P v.
proof: Proof. intros P a n v. split. - rewrite !Forall_forall. intros H. split. + apply H, In_cons_hd. + intros b Hb. apply H, In_cons_tl, Hb. - intros [??]. now constructor. Qed.
imports: VectorDef PeanoNat Eqdep_dec