proposition: Lemma Pf_add_of_list a (l : list A) : Pf_add a (Pf_of_list l) =f= Pf_of_list (a :: l).
proof: Proof. unfold Pf_equiv; simpl. rewrite <- of_cons. refl. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)