get rid of axiomatized by
in favor of [opaque]
with trivial lemma
#681
+124
−84
Loading