An exact proof term for the current goal is and3I (∀X, Obj X → comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (T1 (T0 (T0 X)) (T0 X) (mu X)) = comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (mu (T0 X))) (∀X, Obj X → comp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (eta (T0 X)) = id (T0 X)) (∀X, Obj X → comp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (T1 X (T0 X) (eta X)) = id (T0 X)).