proposition: Lemma in_ind e (P: list X -> Prop): (forall A, P (e :: A)) -> (forall a A, P A -> P (a :: A)) -> forall A, e ∈ A -> P A.
proof: Proof. intros BH IH; induction A; cbn; intuition idtac; subst; intuition (auto with listdb). Qed.
imports: List Arith Lia Morphisms FinFun Init.Wf Undecidability.HOU(std.decidable)