proposition: Lemma pfun_equiv_equiv : forall A B (E:binary B) (P:A->Prop), equiv E -> equiv (@pfun_equiv A B E P).
proof: Proof. Proof using. introv [RE SE TE]. unfold pfun_equiv. constructor; intros_all*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)