proposition: Lemma In_cases {A:Type}{n:nat} (v: t A (S n)) : forall x, In x v -> x = hd v \/ In x (tl v).
proof: Proof. intros; rewrite (decomp _ _ v) in *. inversion H. - left; auto. - apply Eqdep_dec.inj_pair2_eq_dec in H3. + right; cbn; now subst. + decide equality. Qed.