Nuprl Lemma : st-atoms-distinct_wf
∀[T:Id ⟶ Type]. ∀[tab:secret-table(T)].  (atoms-distinct(tab) ∈ ℙ)
Proof
Definitions occuring in Statement : 
st-atoms-distinct: atoms-distinct(tab)
, 
secret-table: secret-table(T)
, 
Id: Id
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
member: t ∈ T
, 
function: x:A ⟶ B[x]
, 
universe: Type
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
st-atoms-distinct: atoms-distinct(tab)
, 
subtype_rel: A ⊆r B
, 
so_lambda: λ2x.t[x]
, 
implies: P 
⇒ Q
, 
prop: ℙ
, 
int_seg: {i..j-}
, 
so_apply: x[s]
Latex:
\mforall{}[T:Id  {}\mrightarrow{}  Type].  \mforall{}[tab:secret-table(T)].    (atoms-distinct(tab)  \mmember{}  \mBbbP{})
Date html generated:
2016_05_16-AM-10_02_19
Last ObjectModification:
2015_12_28-PM-09_28_32
Theory : new!event-ordering
Home
Index