Exists
======

.. currentmodule:: proveit.logic

.. autoclass:: Exists
   :show-inheritance:

   .. rubric:: Attributes Summary

   .. autosummary::

      ~Exists.known_instance_maps
      ~Exists.skolem_consts_to_existential

   .. rubric:: Methods Summary

   .. autosummary::

      ~Exists.choose
      ~Exists.conclude
      ~Exists.conclude_via_domain_inclusion
      ~Exists.conclude_via_example
      ~Exists.deduce_in_bool
      ~Exists.deduce_not_exists
      ~Exists.definition
      ~Exists.derive_negated_forall
      ~Exists.elim_domain
      ~Exists.eliminate
      ~Exists.negation_side_effects
      ~Exists.side_effects
      ~Exists.substitute_domain
      ~Exists.substitute_instances
      ~Exists.unfold

   .. rubric:: Attributes Documentation

   .. autoattribute:: known_instance_maps
   .. autoattribute:: skolem_consts_to_existential

   .. rubric:: Methods Documentation

   .. automethod:: choose
   .. automethod:: conclude
   .. automethod:: conclude_via_domain_inclusion
   .. automethod:: conclude_via_example
   .. automethod:: deduce_in_bool
   .. automethod:: deduce_not_exists
   .. automethod:: definition
   .. automethod:: derive_negated_forall
   .. automethod:: elim_domain
   .. automethod:: eliminate
   .. automethod:: negation_side_effects
   .. automethod:: side_effects
   .. automethod:: substitute_domain
   .. automethod:: substitute_instances
   .. automethod:: unfold