Nuprl Rule : applyLambdaEquality

  This rule combines the rules applyEquality and Error :lambdaEquality
but generates one fewer subgoal because the subgoal H  ⊢ A = A  generated
by `lambdaEquality` is not needed because the subgoal H  ⊢ a1 = a2
generated by `applyEquality` also implies that A is a type.
⋅

H  ⊢ ((λx1.b1) a1) = ((λx2.b2) a2) ∈ B[a1/x]

  BY applyLambdaEquality z (x:A ⟶ B) ()

  H z:A ⊢ b1[z/x1] = b2[z/x2] ∈ B[z/x]
  H  ⊢ a1 = a2 ∈ A

Definitions occuring in rule : apply: f a, lambda: λx.A[x], function: x:A ⟶ B[x], equal: s = t ∈ T, axiom: Ax

Latex:
H \mvdash{} ((\mlambda{}x1.b1) a1) = ((\mlambda{}x2.b2) a2) BY applyLambdaEquality z (x:A {}\mrightarrow{} B) () H z:A \mvdash{} b1[z/x1] = b2[z/x2] H \mvdash{} a1 = a2 Date html generated: 2019_06_20-PM-04_11_47 Last ObjectModification: 2016_07_09-PM-11_30_46 Theory : rules Home Index