proposition: Lemma Pf_equiv_of {P Q : Pf} : P [=] Q -> P =f= Q.
proof: Proof. unfold Pf_equiv. auto. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)