proposition: Lemma list_in_decb_iff (l : list X) : forall x, list_in_decb l x = true <-> x el l.
proof: Proof. Proof using eqb_correct. intros x. induction l. - cbn. firstorder. - split. + intros [H1 | H1]%orb_true_elim. left. now apply eqb_correct. apply IHl in H1. now right. + intros [H | H]. cbn. apply orb_true_intro; left; now apply eqb_correct. cbn. apply orb_true_intro; right; now apply IHl. Qed.
imports: Undecidability.L.Tactics(LTactics) Undecidability.L(Functions.EqBool)