Assume Heta HH.
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'' (F0 (H0 X)) (G0 (H0 X)) (eta (H0 X)).
Apply Heta1 to the current goal.
We will prove Obj' (H0 X).
Apply HH1 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'' (F0 (H0 X)) (G0 (H0 X)) (G0 (H0 Y)) (G1 (H0 X) (H0 Y) (H1 X Y f)) (eta (H0 X)) = comp'' (F0 (H0 X)) (F0 (H0 Y)) (G0 (H0 Y)) (eta (H0 Y)) (F1 (H0 X) (H0 Y) (H1 X Y f)).
Apply Heta2 (H0 X) (H0 Y) (H1 X Y f) to the current goal.
Apply HH1 to the current goal.
An exact proof term for the current goal is HX.
Apply HH1 to the current goal.
An exact proof term for the current goal is HY.
Apply HH2 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.
∎