Nuprl - Proof: comp2 comp assoc

A,A',B,C,B',C':Type, h:(A'A), g:(ABC), f1:(BB'), f2:(CC'). (f1,f2) o g o h = (f1,f2) o g o h

By: Auto THEN Ext THEN Reduce 0 THEN GenConclAtAddr [2;1] THEN Analyze -2 THEN Reduce 0

Generated subgoals:

None

About: