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 ⟶ ext λz.b

  BY lambdaFormation !parameter{i:l} ()
  
  z:A @i ⊢ B[z/x] ext b
  H  ⊢ A ∈ Type



Definitions occuring in rule :  function: x:A ⟶ B[x] lambda: λx.A[x] equal: 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  @i  \mvdash{}  B[z/x]  ext  b
    H    \mvdash{}  A  =  A



Date html generated: 2016_12_14-AM-08_53_23
Last ObjectModification: 2016_07_08-PM-03_48_52

Theory : rules


Home Index