Assume HC.
Apply MetaCat_E Obj Hom id comp HC to the current goal.
Assume HC1: ∀X : set, Obj X → Hom X X (id X).
Assume HC2: ∀X Y Z : set, ∀f g : set, Obj X → Obj Y → Obj Z → Hom X Y f → Hom Y Z g → Hom X Z (comp X Y Z g f).
Assume HC3: ∀X Y : set, ∀f : set, Obj X → Obj Y → Hom X Y f → comp X X Y f (id X) = f.
Assume HC4: ∀X Y : set, ∀f : set, Obj X → Obj Y → Hom X Y f → comp X Y Y (id Y) f = f.
Assume HC5: ∀X Y Z W : set, ∀f g h : set, Obj X → Obj Y → Obj Z → Obj W → Hom X Y f → Hom Y Z g → Hom Z W h → comp X Y W (comp Y Z W h g) f = comp X Z W h (comp X Y Z g f).
An exact proof term for the current goal is HC1.
Let X, Y, Z, f and g be given.
Assume HX HY HZ Hf Hg.
An exact proof term for the current goal is HC2 Z Y X g f HZ HY HX Hg Hf.
Let X, Y and f be given.
Assume HX HY Hf.
An exact proof term for the current goal is HC4 Y X f HY HX Hf.
Let X, Y and f be given.
Assume HX HY Hf.
An exact proof term for the current goal is HC3 Y X f HY HX Hf.
Let X, Y, Z, W, f, g and h be given.
Assume HX HY HZ HW Hf Hg Hh.
We will prove comp W Y X f (comp W Z Y g h) = comp W Z X (comp Z Y X f g) h.
Use symmetry.
An exact proof term for the current goal is HC5 W Z Y X h g f HW HZ HY HX Hh Hg Hf.