Assume HF HG.
Apply MetaFunctorE Obj Hom id comp Obj' Hom' id' comp' F0 F1 HF to the current goal.
Assume HF1 HF2 HF3 HF4.
Apply MetaFunctorE Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' G0 G1 HG to the current goal.
Assume HG1 HG2 HG3 HG4.
Let X be given.
Assume HX.
We will prove Obj'' (G0 (F0 X)).
Apply HG1 to the current goal.
Apply HF1 to the current goal.
An exact proof term for the current goal is HX.
Let X, Y and f be given.
Assume HX HY Hf.
We will prove Hom'' (G0 (F0 X)) (G0 (F0 Y)) (G1 (F0 X) (F0 Y) (F1 X Y f)).
Apply HG2 to the current goal.
Apply HF1 to the current goal.
An exact proof term for the current goal is HX.
Apply HF1 to the current goal.
An exact proof term for the current goal is HY.
Apply HF2 to the current goal.
An exact proof term for the current goal is HX.
An exact proof term for the current goal is HY.
An exact proof term for the current goal is Hf.
Let X be given.
Assume HX.
We will prove G1 (F0 X) (F0 X) (F1 X X (id X)) = id'' (G0 (F0 X)).
Use transitivity with and G1 (F0 X) (F0 X) (id' (F0 X)).
Use f_equal.
An exact proof term for the current goal is HF3 X HX.
An exact proof term for the current goal is HG3 (F0 X) (HF1 X HX).
Let X, Y, Z, f and g be given.
Assume HX HY HZ Hf Hg.
We will prove G1 (F0 X) (F0 Z) (F1 X Z (comp X Y Z g f)) = comp'' (G0 (F0 X)) (G0 (F0 Y)) (G0 (F0 Z)) (G1 (F0 Y) (F0 Z) (F1 Y Z g)) (G1 (F0 X) (F0 Y) (F1 X Y f)).
Use transitivity with and G1 (F0 X) (F0 Z) (comp' (F0 X) (F0 Y) (F0 Z) (F1 Y Z g) (F1 X Y f)).
Use f_equal.
An exact proof term for the current goal is HF4 X Y Z f g HX HY HZ Hf Hg.
Apply HG4 (F0 X) (F0 Y) (F0 Z) (F1 X Y f) (F1 Y Z g) (HF1 X HX) (HF1 Y HY) (HF1 Z HZ) to the current goal.
An exact proof term for the current goal is HF2 X Y f HX HY Hf.
An exact proof term for the current goal is HF2 Y Z g HY HZ Hg.