Assume HF HG Heta HH.
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.
Apply MetaNatTransE Obj Hom id comp Obj' Hom' id' comp' F0 F1 G0 G1 eta Heta to the current goal.
Assume Heta1 Heta2.
Apply MetaFunctorE Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' H0 H1 HH to the current goal.
Assume HH1 HH2 HH3 HH4.
Apply MetaNatTransI to the current goal.
Let X be given.
Assume HX.
We will prove Hom'' (H0 (F0 X)) (H0 (G0 X)) (H1 (F0 X) (G0 X) (eta X)).
Apply HH2 to the current goal.
We will prove Obj' (F0 X).
Apply HF1 to the current goal.
An exact proof term for the current goal is HX.
We will prove Obj' (G0 X).
Apply HG1 to the current goal.
An exact proof term for the current goal is HX.
We will prove Hom' (F0 X) (G0 X) (eta X).
Apply Heta1 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 comp'' (H0 (F0 X)) (H0 (G0 X)) (H0 (G0 Y)) (H1 (G0 X) (G0 Y) (G1 X Y f)) (H1 (F0 X) (G0 X) (eta X)) = comp'' (H0 (F0 X)) (H0 (F0 Y)) (H0 (G0 Y)) (H1 (F0 Y) (G0 Y) (eta Y)) (H1 (F0 X) (F0 Y) (F1 X Y f)).
Use transitivity with H1 (F0 X) (G0 Y) (comp' (F0 X) (G0 X) (G0 Y) (G1 X Y f) (eta X)), and H1 (F0 X) (G0 Y) (comp' (F0 X) (F0 Y) (G0 Y) (eta Y) (F1 X Y f)).
Use symmetry.
Apply HH4 to the current goal.
Apply HF1 to the current goal.
An exact proof term for the current goal is HX.
Apply HG1 to the current goal.
An exact proof term for the current goal is HX.
Apply HG1 to the current goal.
An exact proof term for the current goal is HY.
An exact proof term for the current goal is Heta1 X HX.
An exact proof term for the current goal is HG2 X Y f HX HY Hf.
Use f_equal.
An exact proof term for the current goal is Heta2 X Y f HX HY Hf.
Apply HH4 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 HG1 to the current goal.
An exact proof term for the current goal is HY.
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 Heta1 Y HY.
∎