Nuprl Rule : lambdaFormation

Nuprl Rule : lambdaFormation_alt

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_alt z ()

  H z:A ⊢ B[z/x] ext b
  H  ⊢ istype(A)

Latex:
H \mvdash{} x:A {}\mrightarrow{} B ext \mlambda{}z.b BY lambdaFormation\_alt z () H z:A \mvdash{} B[z/x] ext b H \mvdash{} istype(A) Date html generated: 2019_06_20-PM-04_11_40 Last ObjectModification: 2018_09_25-PM-02_11_28 Theory : rules Home Index