Nuprl Lemma : vr_test_ackn'base_wf
vr_test_ackn'base() 
 EClass'(Unit)
Proof not projected
Definitions occuring in Statement : 
vr_test_ackn'base: vr_test_ackn'base(), 
Message: Message, 
eclass: EClass(A[eo; e]), 
unit: Unit, 
member: t 
 T
Definitions : 
member: t 
 T, 
vr_test_ackn'base: vr_test_ackn'base(), 
name: Name, 
uall:
[x:A]. B[x]
Lemmas : 
base-headers-msg-val_wf, 
unit_wf2
vr\_test\_ackn'base()  \mmember{}  EClass'(Unit)
Date html generated:
2012_02_20-PM-07_45_06
Last ObjectModification:
2012_02_03-PM-08_21_08
Home
Index