fact: Definition Pf_equiv_of2 {P Q : Pf} := Pf_equiv_of_gen P Q (reflexivity _) (reflexivity _).
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)