Theorems (or conjectures) for the theory of proveit.core_expr_types.lambda_maps

import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import Conditional, Lambda
from proveit import i, a, b, c, f, g, Q
from proveit.core_expr_types import (
    a_1_to_i, b_1_to_i, c_1_to_i, 
    f__a_1_to_i, g__a_1_to_i, f__b_1_to_i, g__c_1_to_i,
    Q__a_1_to_i, Q__b_1_to_i, Q__c_1_to_i)
from proveit.logic import Forall, Implies, Equals
from proveit.numbers import NaturalPos

%begin theorems

Defining theorems for theory 'proveit.core_expr_types.lambda_maps'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

general_lambda_substitution = \
    Forall(i, Forall((f, g, Q), 
                     Implies(Forall(a_1_to_i, 
                                    Equals(f__a_1_to_i, 
                                           g__a_1_to_i), 
                                    conditions = [Q__a_1_to_i]),
                             Equals(Lambda(b_1_to_i, 
                                           Conditional(f__b_1_to_i, 
                                                       Q__b_1_to_i)),
                                    Lambda(c_1_to_i, 
                                           Conditional(g__c_1_to_i, 
                                                       Q__c_1_to_i))) \
                                      .with_wrap_after_operator()).with_wrap_after_operator()),
          domain=NaturalPos)

general_lambda_substitution (conjecture without proof):

%end theorems

These theorems may now be imported from the theory package: proveit.core_expr_types.lambda_maps