### Nuprl Lemma : oob-getright_wf

`∀[B,A:Type]. ∀[x:{x:one_or_both(A;B)| ↑oob-hasright(x)} ].  (oob-getright(x) ∈ B)`

Proof

Definitions occuring in Statement :  oob-getright: `oob-getright(x)` oob-hasright: `oob-hasright(x)` one_or_both: `one_or_both(A;B)` assert: `↑b` uall: `∀[x:A]. B[x]` member: `t ∈ T` set: `{x:A| B[x]} ` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` oob-getright: `oob-getright(x)` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` ifthenelse: `if b then t else f fi ` bfalse: `ff` so_lambda: `λ2x.t[x]` so_apply: `x[s]` prop: `ℙ` oob-hasright: `oob-hasright(x)` or: `P ∨ Q` not: `¬A` false: `False`
Lemmas referenced :  oobright?_wf bool_wf eqtt_to_assert oobright-rval_wf uiff_transitivity equal-wf-T-base assert_wf bnot_wf not_wf eqff_to_assert assert_of_bnot pi2_wf oobboth-bval_wf equal_wf set_wf one_or_both_wf oob-hasright_wf assert_of_bor oobboth?_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut setElimination thin rename sqequalRule extract_by_obid sqequalHypSubstitution isectElimination cumulativity hypothesisEquality hypothesis lambdaFormation unionElimination equalityElimination because_Cache productElimination independent_isectElimination equalityTransitivity equalitySymmetry baseClosed independent_functionElimination lambdaEquality dependent_functionElimination axiomEquality isect_memberEquality universeEquality voidElimination

Latex:
\mforall{}[B,A:Type].  \mforall{}[x:\{x:one\_or\_both(A;B)|  \muparrow{}oob-hasright(x)\}  ].    (oob-getright(x)  \mmember{}  B)

Date html generated: 2018_05_21-PM-08_00_12
Last ObjectModification: 2017_07_26-PM-05_37_03

Theory : general

Home Index