I'm not sure if this is related to #304 but I tried to make my own hopf to introduce CNOTs since the CNOT introduction does not always respect the ordering of the controls vs the targets. But the double edge isn't stored in the rewrite rule.

This is the rewrite rule:

This is how the rule is loaded in the proof system: