Nuprl Definition : W-null

W-null(eq;a0;w) ==  eq a0 (fst(w))


Definitions occuring in Statement :  pi1: fst(t),  apply: f a
Definitions occuring in definition :  apply: f a,  pi1: fst(t)
FDL editor aliases :  W-null
Latex:
W-null(eq;a0;w)  ==    eq  a0  (fst(w))


Date html generated: 2016_05_15-PM-10_06_39
Last ObjectModification: 2015_09_23-AM-08_22_16

Theory : bar!induction


Home Index