proposition: Lemma pIn_split_r {A B : Type} (lst : plist (pprod A B)) (p : pprod A B) (H : pIn p lst) : (pIn (psnd p) (snd (split lst))).
proof: Proof. destruct p; simpl. induction lst; simpl in *. + destruct H. + destruct t; simpl. destruct (split lst); simpl. destruct H. { inv_all; tauto. } { tauto. } 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