Nuprl Rule : dependent_functionElimination

f:(x:A ⟶ B) @lvl, J ⊢ ext !((!\y,v.t) Ax)

  BY dependent_functionElimination #$i v
  
  f:(x:A ⟶ B), J ⊢ a ∈ A
  f:(x:A ⟶ B), J, y:B[a/x] @lvl, v:(y (f a) ∈ B[a/x]) ⊢ ext t



Definitions occuring in rule :  axiom: Ax function: x:A ⟶ B[x] equal: t ∈ T apply: a

Latex:
H  f:(x:A  {}\mrightarrow{}  B)  @lvl,  J  \mvdash{}  T  ext  !((!\mbackslash{}y,v.t)  f  a  Ax)

    BY  dependent\_functionElimination  \#\$i  a  y  v
   
    H  f:(x:A  {}\mrightarrow{}  B),  J  \mvdash{}  a  =  a
    H  f:(x:A  {}\mrightarrow{}  B),  J,  y:B[a/x]  @lvl,  v:(y  =  (f  a))  \mvdash{}  T  ext  t



Date html generated: 2016_12_14-AM-08_53_25
Last ObjectModification: 2015_11_25-PM-03_37_44

Theory : rules


Home Index