proposition: Lemma In_cons_iff A: forall n a b (v : t A n), In a (b :: v) <-> (b = a \/ In a v).
proof: Proof. intros n a b v. split. - enough (H : forall n (v : t A n), In a v -> match v with | nil _ => False | cons _ b _ v => b = a \/ In a v end) by apply H. now intros ?? []; [left|right]. - intros [<-|?]. + apply In_cons_hd. + now apply In_cons_tl. Qed.
imports: VectorDef PeanoNat Eqdep_dec