Demonstrations for the theory of proveit.core_expr_types.lambda_maps

import proveit
from proveit import Lambda, Conditional
from proveit import x, fx, gx, Qx
from proveit.logic import Equals, Forall
%begin demonstrations

Lambda substitution

universal_eq = Forall(x, Equals(fx, gx))

universal_eq:

Lambda(x, fx).substitution(universal_eq, assumptions=[universal_eq])

 ⊢  

universal_eq_with_cond = Forall(x, Equals(fx, gx), condition=Qx)

universal_eq_with_cond:

Lambda(x, Conditional(fx, Qx)).substitution(universal_eq_with_cond, 
                                            assumptions=[universal_eq_with_cond])

 ⊢  

%end demonstrations