Nuprl Lemma : pi-example-inst_wf
pi-example-inst() ∈ pi_term()
Proof
Definitions occuring in Statement :
pi-example-inst: pi-example-inst(),
pi_term: pi_term(),
member: t ∈ T
Definitions unfolded in proof :
pi-example-inst: pi-example-inst(),
member: t ∈ T,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
listp: A List+,
name: Name
Latex:
pi-example-inst() \mmember{} pi\_term()
Date html generated:
2016_05_17-AM-11_23_26
Last ObjectModification:
2015_12_29-PM-06_54_13
Theory : event-logic-applications
Home
Index