proposition: Lemma pIn_app_iff (A : Type) (l l' : plist A) (a : A) : pIn a (app l l') <-> pIn a l \/ pIn a l'.
proof: Proof. induction l; simpl; intuition congruence. 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