Nuprl Rule : lambdaFormation
This rule proved as lemma rule_lambda_formation_true in file rules/rules_function.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ x:A ⟶ B ext λz.b
BY lambdaFormation !parameter{i:l} z ()
H z:A ⊢ B[z/x] ext b
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{} x:A {}\mrightarrow{} B ext \mlambda{}z.b
BY lambdaFormation !parameter\{i:l\} z ()
H z:A \mvdash{} B[z/x] ext b
H \mvdash{} A = A
Date html generated:
2019_06_20-PM-04_11_47
Last ObjectModification:
2018_09_25-PM-01_50_50
Theory : rules
Home
Index