proposition: Lemma card_ind (P : Pf -> Prop) (H : forall n X, card X = n -> P X) : forall X, P X.
proof: Proof. intro X. eapply H. refl. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)