Nuprl Lemma : RightComb_wf
[A:Type]. (RightComb(A) 
CombinatorDef)
Proof not projected
Definitions occuring in Statement :
RightComb: RightComb(A),
combinator-def: CombinatorDef,
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
implies: P 
Q,
member: t T,
all: x:A. B[x],
uall: [x:A]. B[x]
Lemmas :
isl_wf,
top_wf
\mforall{}[A:Type]. (RightComb(A) \mmember{} CombinatorDef)
Date html generated:
2012_01_23-PM-01_32_59
Last ObjectModification:
2011_12_11-PM-12_20_43
Home
Index