Nuprl Lemma : outl_wf

[A,B:Type]. ∀[x:A B].  outl(x) ∈ supposing ↑isl(x)


Proof




Definitions occuring in Statement :  outl: outl(x) assert: b isl: isl(x) uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T union: left right universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a outl: outl(x) isl: isl(x) assert: b ifthenelse: if then else fi  bfalse: ff false: False prop:
Lemmas referenced :  assert_wf isl_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut unionElimination thin sqequalRule sqequalHypSubstitution hypothesisEquality voidElimination hypothesis axiomEquality equalityTransitivity equalitySymmetry lemma_by_obid isectElimination isect_memberEquality because_Cache unionEquality universeEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[x:A  +  B].    outl(x)  \mmember{}  A  supposing  \muparrow{}isl(x)



Date html generated: 2016_05_13-PM-03_20_22
Last ObjectModification: 2015_12_26-AM-09_10_51

Theory : union


Home Index