Nuprl Lemma : eqtt_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] equal: t ∈ 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 sq_type: SQType(T) guard: {T} subtype_rel: A ⊆B rev_implies:  Q iff: ⇐⇒ Q
Lemmas referenced :  bool_wf true_wf false_wf equal_wf equal-wf-T-base assert_wf subtype_base_sq bool_subtype_base btrue_wf iff_weakening_uiff sqequal-wf-base sqeqtt_to_assert uiff_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality isect_memberEquality isectElimination hypothesisEquality extract_by_obid hypothesis lambdaFormation unionElimination axiomEquality equalityTransitivity equalitySymmetry voidElimination dependent_functionElimination independent_functionElimination baseClosed independent_pairFormation instantiate cumulativity independent_isectElimination sqequalAxiom sqequalIntensionalEquality applyEquality addLevel because_Cache

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



Date html generated: 2017_04_14-AM-07_14_15
Last ObjectModification: 2017_02_27-PM-02_50_02

Theory : union


Home Index