proposition: Lemma Forall_forall {A:Type}(P: A -> Prop) : forall {n:nat} (v: t A n) , Forall P v <-> (forall a, In a v -> P a).
proof: Proof. induction n. - intro v; rewrite (t_0_nil _ v). split. + inversion 2. + left. - intro v; rewrite (decomp _ _ v); split. + intros H a H0; destruct (Forall_and _ _ H ). destruct (In_cases _ _ H0) as [H3 | H3]. * now subst. * cbn in H2; rewrite IHn in H2; apply H2, H3. + intros H; right. * apply H; left. * rewrite IHn; auto. intros; apply H. right; auto. Qed.