Nuprl Lemma : bool_sim_true

[b:𝔹]. tt supposing tt


Proof




Definitions occuring in Statement :  btrue: tt bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] sqequal: t equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a sq_type: SQType(T) all: x:A. B[x] implies:  Q guard: {T} prop:
Lemmas referenced :  subtype_base_sq bool_wf bool_subtype_base equal_wf btrue_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin instantiate lemma_by_obid sqequalHypSubstitution isectElimination cumulativity hypothesis independent_isectElimination dependent_functionElimination hypothesisEquality equalityTransitivity equalitySymmetry independent_functionElimination sqequalAxiom sqequalRule isect_memberEquality because_Cache

Latex:
\mforall{}[b:\mBbbB{}].  b  \msim{}  tt  supposing  b  =  tt



Date html generated: 2016_05_13-PM-03_55_24
Last ObjectModification: 2015_12_26-AM-10_53_12

Theory : bool_1


Home Index