Nuprl Rule : dependent_functionElimination
H f:(x:A ⟶ B), J ⊢ T ext !((!\y,v.t) f a Ax)
BY dependent_functionElimination #$i a y v
H f:(x:A ⟶ B), J ⊢ a = a ∈ A
H f:(x:A ⟶ B), J, y:B[a/x], v:(y = (f a) ∈ B[a/x]) ⊢ T ext t
Definitions occuring in rule :
axiom: Ax,
function: x:A ⟶ B[x],
equal: s = t ∈ T,
apply: f a
Latex:
H f:(x:A {}\mrightarrow{} B), 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], v:(y = (f a)) \mvdash{} T ext t
Date html generated:
2019_06_20-PM-04_11_42
Last ObjectModification:
2018_08_24-PM-04_28_16
Theory : rules
Home
Index