Nuprl Lemma : sqeqtt_to_assert

[b:𝔹]. uiff(b tt;↑b)


Proof




Definitions occuring in Statement :  assert: b btrue: tt bool: 𝔹 uiff: uiff(P;Q) uall: [x:A]. B[x] sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a assert: b ifthenelse: if then else fi  all: x:A. B[x] implies:  Q bool: 𝔹 true: True prop: false: False subtype_rel: A ⊆B unit: Unit it: btrue: tt bfalse: ff sq_type: SQType(T) guard: {T}
Lemmas referenced :  assert_of_tt true_wf false_wf equal_wf bool_subtype_base subtype_base_sq bool_wf btrue_wf assert_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation hypothesis extract_by_obid sqequalRule sqequalHypSubstitution thin because_Cache lambdaFormation unionElimination axiomEquality equalityTransitivity equalitySymmetry isectElimination hypothesisEquality dependent_functionElimination independent_functionElimination sqequalIntensionalEquality applyEquality baseClosed instantiate cumulativity independent_isectElimination equalityElimination voidElimination sqequalAxiom productElimination independent_pairEquality isect_memberEquality

Latex:
\mforall{}[b:\mBbbB{}].  uiff(b  \msim{}  tt;\muparrow{}b)



Date html generated: 2017_04_14-AM-07_14_12
Last ObjectModification: 2017_02_27-PM-02_49_58

Theory : union


Home Index