### Nuprl Lemma : atom2-deq-aux

`∀[a,b:Atom2].  uiff(a = b ∈ Atom2;↑a =a2 b)`

Proof

Definitions occuring in Statement :  eq_atom: `eq_atom\$n(x;y)` atom: `Atom\$n` assert: `↑b` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` rev_uimplies: `rev_uimplies(P;Q)` implies: `P `` Q` prop: `ℙ`
Lemmas referenced :  assert_of_eq_atom2 assert_witness eq_atom_wf2 equal_wf assert_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis productElimination independent_isectElimination independent_functionElimination atomnEquality sqequalRule independent_pairEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry axiomEquality

Latex:
\mforall{}[a,b:Atom2].    uiff(a  =  b;\muparrow{}a  =a2  b)

Date html generated: 2016_05_14-PM-03_33_46
Last ObjectModification: 2015_12_26-PM-06_00_57

Theory : decidable!equality

Home Index