Nuprl - Proof: hrep sum inj 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hrep sum inj 1

1. 'a : S
2. 'b : S
3. u : 'a+'b
4. v : 'a+'b
5. rep_sum(u) = rep_sum(v)

u = v

By:	Inst Thm: hsum iso def ['a;'b] THEN Simpset [`hol_to_nuprl`] THEN Simp THEN StrongAuto

Generated subgoal:

1 6. a:hsum('a; 'b). abs_sum(rep_sum(a)) = a
7. r:(hbool  'a  'b  hbool).
7. is_sum_rep(r) = ((rep_sum(abs_sum(r))) = r)  hbool
  u = v
3 steps

About:

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