proposition: Lemma Pf_eq_of_list (P : Pf) : P =f= Pf_of_list (list_of_finite P).
proof: Proof. apply finite_eq_of_list. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)