Nuprl Lemma : band-inl

[a,b:Top].  ((inl a) ∧b b)


Proof




Definitions occuring in Statement :  band: p ∧b q uall: [x:A]. B[x] top: Top inl: inl x sqequal: t
Definitions unfolded in proof :  band: p ∧b q 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].    ((inl  a)  \mwedge{}\msubb{}  b  \msim{}  b)



Date html generated: 2016_05_13-PM-03_59_23
Last ObjectModification: 2015_12_26-AM-10_50_34

Theory : bool_1


Home Index