Nuprl Lemma : loopset-sq
loopset() ~ mk-coset(Unit;λp.loopset())
Proof
Definitions occuring in Statement : 
loopset: loopset()
, 
mk-coset: mk-coset(T;f)
, 
unit: Unit
, 
lambda: λx.A[x]
, 
sqequal: s ~ t
Definitions unfolded in proof : 
member: t ∈ T
, 
unit: Unit
, 
mk-coset: mk-coset(T;f)
, 
loopset: loopset()
Rules used in proof : 
sqequalReflexivity, 
computationStep, 
sqequalTransitivity, 
sqequalRule, 
sqequalSubstitution
Latex:
loopset()  \msim{}  mk-coset(Unit;\mlambda{}p.loopset())
Date html generated:
2018_07_29-AM-09_50_27
Last ObjectModification:
2018_07_21-PM-00_11_30
Theory : constructive!set!theory
Home
Index