Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ιο be given.
Let x1 of type ιιιο be given.
Let x2 of type ιι be given.
Let x3 of type ιιιιιι be given.
Let x4 of type ιο be given.
Let x5 of type ιιιο be given.
Let x6 of type ιι be given.
Let x7 of type ιιιιιι be given.
Let x8 of type ιι be given.
Let x9 of type ιιιι be given.
Let x10 of type ιι be given.
Let x11 of type ιιιι be given.
Let x12 of type ιι be given.
Assume H0: MetaNatTrans_buggy_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12.
Apply and5E with MetaCat x0 x1 x2 x3, MetaCat x4 x5 x6 x7, MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x10 x11, MetaNatTrans_buggy x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12.
The subproof is completed by applying H0.