Nuprl Lemma : eq_atom1_self

[x:Atom1]. (x =a1 tt)


Proof




Definitions occuring in Statement :  eq_atom: eq_atom$n(x;y) atom: Atom$n btrue: tt uall: [x:A]. B[x] sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a uiff: uiff(P;Q) and: P ∧ Q sq_type: SQType(T) all: x:A. B[x] implies:  Q guard: {T} rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  subtype_base_sq bool_subtype_base eqtt_to_assert eq_atom_wf1 assert_of_eq_atom1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin instantiate lemma_by_obid sqequalHypSubstitution isectElimination because_Cache independent_isectElimination hypothesis hypothesisEquality productElimination dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination sqequalAxiom atomnEquality

Latex:
\mforall{}[x:Atom1].  (x  =a1  x  \msim{}  tt)



Date html generated: 2016_05_13-PM-03_21_15
Last ObjectModification: 2015_12_26-AM-09_12_02

Theory : atom_1


Home Index