Nuprl Lemma : Id_wf
Id ∈ Type
Proof
Definitions occuring in Statement :
Id: Id,
member: t ∈ T,
universe: Type
Definitions unfolded in proof :
Id: Id,
member: t ∈ T
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
atomnEquality
Latex:
Id \mmember{} Type
Date html generated:
2016_05_14-PM-03_36_35
Last ObjectModification:
2015_12_26-PM-05_59_19
Theory : decidable!equality
Home
Index