proposition: Lemma Forall_and {A:Type}(P: A -> Prop) {n:nat} (v: t A (S n)) : Forall P v -> P (hd v) /\ Forall P (tl v).
proof: Proof. rewrite (decomp _ _ v); cbn. inversion 1; split; auto. apply Eqdep_dec.inj_pair2_eq_dec in H2; subst; auto. decide equality. Qed.