Nuprl - Proof: mul via intseg one 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: mul via intseg one 1 1

1. a :

2. b :

3. e : {a..b

}

i:{a..b

}. e(i) = 1

is_ident(

; (

x,y. x

y); 1)

By:	BackThru: Thm* is_ident(; (x,y. xy); 1)

Generated subgoals:

None

About:

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