mathlib3

6de3506c - new proof of `oplax_nat_trans.vcomp`