At:
comp2 comp2 assoc A1,A2,A',B,C,B',C':Type, h:(A'A1A2), g1:(A1B), g2:(A2C), f1:(BB'), f2:(CC'). (f1,f2) o (g1,g2) o h = (f1 o g1,f2 o g2) o h
By:
Auto
THEN
Ext
THEN
Reduce 0
THEN
GenConclAtAddr [2;1;1]
THEN
Analyze -2
THEN
Reduce 0
Generated subgoals:
A1,A2,A',B,C,B',C':Type, h:(A'
A1
A2), g1:(A1