Nuprl Lemma : data_wf

[T:Id ⟶ Type]. (data(T) ∈ Type)


Proof




Definitions occuring in Statement :  data: data(T) Id: Id uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T data: data(T)

Latex:
\mforall{}[T:Id  {}\mrightarrow{}  Type].  (data(T)  \mmember{}  Type)



Date html generated: 2016_05_16-AM-09_59_22
Last ObjectModification: 2015_12_28-PM-09_29_56

Theory : new!event-ordering


Home Index