Nuprl Lemma : opt_wf

[T:Type]. ∀[x:T]. ∀[b:𝔹].  ((b?x) ∈ T?)


Proof




Definitions occuring in Statement :  opt: (b?x) bool: 𝔹 uall: [x:A]. B[x] unit: Unit member: t ∈ T union: left right universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T opt: (b?x) all: x:A. B[x] implies:  Q exposed-bfalse: exposed-bfalse bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a ifthenelse: if then else fi  bfalse: ff prop:
Lemmas referenced :  eqtt_to_assert unit_wf2 uiff_transitivity equal-wf-T-base bool_wf assert_wf bnot_wf not_wf eqff_to_assert assert_of_bnot it_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule hypothesisEquality thin because_Cache lambdaFormation sqequalHypSubstitution unionElimination equalityElimination extract_by_obid isectElimination hypothesis productElimination independent_isectElimination inlEquality baseClosed independent_functionElimination inrEquality equalityTransitivity equalitySymmetry dependent_functionElimination axiomEquality universeIsType isect_memberEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[b:\mBbbB{}].    ((b?x)  \mmember{}  T?)



Date html generated: 2019_10_15-AM-10_46_43
Last ObjectModification: 2018_09_27-AM-09_37_27

Theory : basic


Home Index