Nuprl Lemma : id-deq_wf
IdDeq ∈ EqDecider(Id)
Proof
Definitions occuring in Statement :
id-deq: IdDeq,
Id: Id,
deq: EqDecider(T),
member: t ∈ T
Definitions unfolded in proof :
id-deq: IdDeq,
Id: Id,
member: t ∈ T
Lemmas referenced :
atom2-deq_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
lemma_by_obid,
hypothesis
Latex:
IdDeq \mmember{} EqDecider(Id)
Date html generated:
2016_05_14-PM-03_37_07
Last ObjectModification:
2015_12_26-PM-05_58_35
Theory : decidable!equality
Home
Index