A:Type, eq:EqDecider(A), B:(AType), f,g,h:a:A fp-> B(a).
  f || h  g || h  f  g || h

By:	Auto THEN BackThru Thm* eq:EqDecider(A), B:(AType), f,g:a:A fp-> B(a). f || g  g || f THEN BackThru Thm: fpf-compatible-join THEN BackThru Thm* eq:EqDecider(A), B:(AType), f,g:a:A fp-> B(a). f || g  g || f

None

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