proveit.core_expr_types.operations.operands_substitution_via_tuple
proveit.logic.equality.lhs_via_equality