(4steps total) PrintForm Definitions Lemmas hol sum Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hinl def 1
1. 'b : S
2. 'a : S
3. e : 'a
  inl(e) = abs_sum(b:hbool. x:'a. y:'b. (x = e)b)
By: Assert (inl(e) = abs_sum(rep_sum(inl(e)))) THEN StrongAuto

Generated subgoals:

1   inl(e) = abs_sum(rep_sum(inl(e)))  'a+'b
1 step
2 4. inl(e) = abs_sum(rep_sum(inl(e)))  'a+'b
  inl(e) = abs_sum(b:hbool. x:'a. y:'b. (x = e)b)
1 step

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

(4steps total) PrintForm Definitions Lemmas hol sum Sections HOLlib Doc