An exact proof term for the current goal is and3I (MetaNatTrans_strict Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f) T0 T1 eta) (MetaNatTrans_strict Obj Hom id comp Obj Hom id comp (λX ⇒ T0 (T0 X)) (λX Y f ⇒ T1 (T0 X) (T0 Y) (T1 X Y f)) T0 T1 mu) MetaMonad.