proposition: Lemma Pf_ind (P : Pf -> Prop) (P_equiv : Proper (Pf_equiv ==> impl) P) (P0 : P Pf_empty) (PS : forall a (X : Pf), ~mem a X -> P X -> P (Pf_add a X)) : forall X, P X.
proof: Proof. intro X. rewrite Pf_equiv_of_list. gen (nodup_list_of_finite X). gen (list_of_finite X). induction l; intro lnd. eapply P_equiv. 2: apply P0. fo. rewrite <- Pf_add_of_list. fo. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)