Quelle  card_power.prf

(card_power
 (card_power 0
  (card_power-1 nil 3316968292
   ("" (rewrite "card_lt_surj")
    (("" (skolem!)
      (("" (expand "surjective?")
        (("" (inst - "{t: T | NOT f!1(t)(t)}")
          (("" (skolem!)
            (("" (decompose-equality)
              (("" (inst - "x!1")
                (("" (iff) (("" (prop) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (surjective? const-decl "bool" functions nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil card_power nil)
    (card_lt_surj formula-decl nil card_comp_props nil))
   shostak)))