Proof of proveit.numbers.exponentiation.exp_eq theorem

import proveit
from proveit import Lambda
from proveit import x, a
from proveit.numbers import Exp
theory = proveit.Theory() # the theorem's theory

%proving exp_eq

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
exp_eq:
(see dependencies)

x_eq_y = exp_eq.conditions[-1]

x_eq_y:

x_eq_y.substitution(Lambda(x, Exp(x, a)), assumptions=[x_eq_y])

 ⊢  

exp_eq may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

%qed

proveit.numbers.exponentiation.exp_eq has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3	⊢
	: , : , :
2	axiom		⊢
	proveit.logic.equality.substitution
3	assumption		⊢