proposition: Lemma Pf_singleton_eq x : Pf_singleton x =f= Pf_add x Pf_empty.
proof: Proof. refl. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)