Nuprl Lemma : set-sig-empty-prop2
∀[Item:Type]. ∀[s:set-sig{i:l}(Item)]. ∀[x:Item].  uiff(↑(set-sig-member(s) x set-sig-empty(s));False)
Proof
Definitions occuring in Statement : 
set-sig-empty: set-sig-empty(s)
, 
set-sig-member: set-sig-member(s)
, 
set-sig: set-sig{i:l}(Item)
, 
assert: ↑b
, 
uiff: uiff(P;Q)
, 
uall: ∀[x:A]. B[x]
, 
false: False
, 
apply: f a
, 
universe: Type
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
uiff: uiff(P;Q)
, 
and: P ∧ Q
, 
uimplies: b supposing a
, 
false: False
, 
not: ¬A
, 
implies: P 
⇒ Q
, 
prop: ℙ
Latex:
\mforall{}[Item:Type].  \mforall{}[s:set-sig\{i:l\}(Item)].  \mforall{}[x:Item].
    uiff(\muparrow{}(set-sig-member(s)  x  set-sig-empty(s));False)
Date html generated:
2016_05_17-PM-01_44_21
Last ObjectModification:
2015_12_28-PM-08_52_33
Theory : datatype-signatures
Home
Index