Proof of proveit.logic.booleans.quantification.existence.exists_unfolding theorem¶
In [1]:
import proveit
from proveit import defaults
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving exists_unfolding
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
exists_unfolding:
(see dependencies)
exists_unfolding:
(see dependencies)
In [3]:
antecedent = exists_unfolding.instance_expr.instance_expr.antecedent
antecedent: 
In [4]:
defaults.assumptions = [exists_unfolding.condition, antecedent]
defaults.assumptions: 
In [5]:
definition = antecedent.definition()
definition: 
⊢ 
⊢ 
In [6]:
definition.derive_right_via_equality().as_implication(antecedent)
