proposition: Lemma inb_sound (x : A) (lst : plist A) (H : inb x lst = true) : pIn x lst.
proof: Proof. induction lst; simpl in *; try congruence. consider (x ?[ eq ] t); intros; subst. + left; reflexivity. + right; apply IHlst; assumption. Qed.
imports: ExtLib.Structures.Functor ExtLib.Structures.Applicative ExtLib.Data.POption ExtLib.Data.PPair ExtLib.Core.RelDec ExtLib.Tactics.Consider ExtLib.Tactics.Injection Coq.Bool.Bool