Nuprl Definition : Wsucc
Wsucc(A;a.B[a];w) == B[fst(w)] ≡ Unit
Definitions occuring in Statement :
ext-eq: A ≡ B,
pi1: fst(t),
unit: Unit
Definitions occuring in definition :
ext-eq: A ≡ B,
pi1: fst(t),
unit: Unit
FDL editor aliases :
Wsucc
Latex:
Wsucc(A;a.B[a];w) == B[fst(w)] \mequiv{} Unit
Date html generated:
2016_05_14-AM-06_16_40
Last ObjectModification:
2015_09_22-PM-05_47_23
Theory : co-recursion
Home
Index