Nuprl - Proof: decidable atom equal 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: decidable atom equal 1 1

1. a : Atom
2. b : Atom

if a=b

Atom

inl(*); inr(

x.x) fi

(a = b

a = b)

By:	MemberEqCD

Generated subgoals:

1   a  Atom
Auto

2   b  Atom
Auto

3 3. a = b
  inl(*)  (a = b  a = b)
3 steps

4 3. a = b
  inr(x.x)  (a = b  a = b)
4 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html