Nuprl Lemma : allowed_provision_lemma
∀v,ok:Top. (allowed(provision(ok; v)) ~ usquash(ok))
Proof
Definitions occuring in Statement :
allowed: allowed(x),
provision: provision(ok; v),
usquash: usquash(T),
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
provision: provision(ok; v),
allowed: allowed(x),
pi1: fst(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. (allowed(provision(ok; v)) \msim{} usquash(ok))
Date html generated:
2020_05_20-AM-08_01_18
Last ObjectModification:
2020_05_17-PM-08_12_09
Theory : monads
Home
Index