Nuprl Lemma : bor-inr

[a,b:Top].  ((inr ) ∨bb)


Proof




Definitions occuring in Statement :  bor: p ∨bq uall: [x:A]. B[x] top: Top inr: inr  sqequal: t
Definitions unfolded in proof :  bor: p ∨bq ifthenelse: if then else fi  uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut sqequalAxiom lemma_by_obid hypothesis sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality because_Cache

Latex:
\mforall{}[a,b:Top].    ((inr  a  )  \mvee{}\msubb{}b  \msim{}  b)



Date html generated: 2016_05_13-PM-03_59_21
Last ObjectModification: 2015_12_26-AM-10_50_24

Theory : bool_1


Home Index