Nuprl Rule : lambdaEquality
This rule proved as lemma rule_lambda_equality_true in file rules/rules_function.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ (λx1.b1) = (λx2.b2) ∈ (x:A ⟶ B)
BY lambdaEquality !parameter{i:l} z ()
H z:A ⊢ b1[z/x1] = b2[z/x2] ∈ B[z/x]
H ⊢ A = A ∈ Type
Definitions occuring in rule :
function: x:A ⟶ B[x],
lambda: λx.A[x],
equal: s = t ∈ T,
universe: Type,
axiom: Ax
Latex:
H \mvdash{} (\mlambda{}x1.b1) = (\mlambda{}x2.b2)
BY lambdaEquality !parameter\{i:l\} z ()
H z:A \mvdash{} b1[z/x1] = b2[z/x2]
H \mvdash{} A = A
Date html generated:
2019_06_20-PM-04_11_48
Last ObjectModification:
2018_09_25-PM-01_40_29
Theory : rules
Home
Index