Nuprl Lemma : allow_provision_lemma
∀v,ok:Top. (allow(provision(ok; v)) ~ v)
Proof
Definitions occuring in Statement :
allow: allow(x),
provision: provision(ok; v),
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
provision: provision(ok; v),
allow: allow(x),
pi2: snd(t),
all: ∀x:A. B[x],
member: t ∈ T
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation_alt,
inhabitedIsType,
hypothesisEquality,
cut,
introduction,
extract_by_obid,
hypothesis
Latex:
\mforall{}v,ok:Top. (allow(provision(ok; v)) \msim{} v)
Date html generated:
2020_05_20-AM-08_01_20
Last ObjectModification:
2020_05_17-PM-08_13_22
Theory : monads
Home
Index