Proof of proveit.logic.equality.multi_substitution theorem

import proveit
from proveit import defaults
from proveit.logic import And
from proveit import a, b, i, n, x, y
from proveit.core_expr_types.tuples import tuple_eq_via_elem_eq
from proveit.core_expr_types.operations  import operands_substitution
theory = proveit.Theory() # the theorem's theory

%proving multi_substitution

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

defaults.assumptions = multi_substitution.all_conditions()

defaults.assumptions:

operands_substitution

 ⊢  

operands_substitution.instantiate({y:y})

,  ⊢  

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

%qed

proveit.logic.equality.multi_substitution has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3, 4	,  ⊢
	: , : , : , :
2	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
3	instantiation	5, 6, 7	⊢
	: , : , :
4	assumption		⊢
5	conjecture		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
6	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
7	assumption		⊢