Proof of proveit.core_expr_types.operations.operator_substitution theorem

import proveit
from proveit import Lambda, f, g, n
from proveit.core_expr_types import x_1_to_n, f__x_1_to_n, g__x_1_to_n
from proveit.logic import Forall, Equals
from proveit.numbers import Natural
theory = proveit.Theory() # the theorem's theory

%proving operator_substitution

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

repl_lambda = Lambda(f, f__x_1_to_n)

repl_lambda:

Equals(f, g).substitution(repl_lambda, assumptions=[Equals(f, g)])

 ⊢  

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

%qed

proveit.core_expr_types.operations.operator_substitution has been proven.

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