Nuprl Lemma : sqequal-tt-to-assert

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


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  btrue: tt true: True implies:  Q iff: ⇐⇒ Q prop: rev_implies:  Q sq_type: SQType(T) all: x:A. B[x] guard: {T}
Lemmas referenced :  assert_witness bool_sq subtype_base_sq bool_subtype_base iff_imp_equal_bool btrue_wf assert_wf true_wf bool_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation hypothesis natural_numberEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination sqequalIntensionalEquality instantiate because_Cache independent_isectElimination sqequalRule lambdaFormation dependent_functionElimination equalityTransitivity equalitySymmetry sqequalAxiom productElimination independent_pairEquality isect_memberEquality

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



Date html generated: 2016_05_15-PM-03_14_34
Last ObjectModification: 2015_12_27-PM-01_02_14

Theory : general


Home Index