import proveit
from proveit import defaults
from proveit.numbers.numerals import DecimalSequence
theory = proveit.Theory() # the theorem's theory
%proving deci_sequence_reduction
defaults.assumptions = deci_sequence_reduction.all_conditions()
equality = defaults.assumptions[-1]
lhs = deci_sequence_reduction.instance_expr.instance_expr.lhs
rhs = deci_sequence_reduction.instance_expr.instance_expr.rhs
equality.substitution(lhs.inner_expr().operands[1])
%qed