Nuprl Lemma : mkid-wf-test
"xxx" ∈ Id
Proof
Definitions occuring in Statement :
mkid: "$x",
Id: Id,
member: t ∈ T
Definitions unfolded in proof :
mkid: "$x",
Id: Id,
member: t ∈ T
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
token2Equality
Latex:
"xxx" \mmember{} Id
Date html generated:
2016_05_14-PM-03_37_01
Last ObjectModification:
2015_12_26-PM-05_58_51
Theory : decidable!equality
Home
Index