Proof of proveit.logic.equality.rhs_via_equality theorem

import proveit
from proveit import defaults, Lambda
from proveit import x, y, P, Q, X
from proveit.logic.equality import sub_right_side_into
theory = proveit.Theory() # the theorem's theory

%proving rhs_via_equality

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

defaults.assumptions = rhs_via_equality.all_conditions()

defaults.assumptions:

sub_right_side_into

 ⊢  

sub_right_side_into.instantiate({P:Lambda(X, X), x:P, y:Q})

,  ⊢  

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

%qed

proveit.logic.equality.rhs_via_equality has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3, 4	,  ⊢
	: , : , :
2	conjecture		⊢
	proveit.logic.equality.sub_right_side_into
3	assumption		⊢
4	assumption		⊢