Nuprl Lemma : es-LnkTag-deq_wf
es-LnkTag-deq ∈ EqDecider(IdLnk × Id)
Proof
Definitions occuring in Statement :
es-LnkTag-deq: es-LnkTag-deq,
IdLnk: IdLnk,
Id: Id,
deq: EqDecider(T),
member: t ∈ T,
product: x:A × B[x]
Lemmas :
product-deq_wf,
IdLnk_wf,
Id_wf,
idlnk-deq_wf,
id-deq_wf
es-LnkTag-deq \mmember{} EqDecider(IdLnk \mtimes{} Id)
Date html generated:
2015_07_17-AM-11_59_53
Last ObjectModification:
2015_01_28-AM-00_35_32
Home
Index