Nuprl Lemma : eq_atom_wf

[x,y:Atom].  (x =a y ∈ 𝔹)


Proof




Definitions occuring in Statement :  eq_atom: =a y bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T atom: Atom
Definitions unfolded in proof :  eq_atom: =a y uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  atom_eq_wf bool_wf btrue_wf bfalse_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis hypothesisEquality axiomEquality equalityTransitivity equalitySymmetry because_Cache isect_memberEquality atomEquality

Latex:
\mforall{}[x,y:Atom].    (x  =a  y  \mmember{}  \mBbbB{})



Date html generated: 2016_05_13-PM-03_20_12
Last ObjectModification: 2015_12_26-AM-09_09_46

Theory : basic_types


Home Index