Prover9 Fold/Unfold

   set(fold_eq).     % use equational defs to introduce defined operation
   set(unfold_eq).   % use equational defs to eliminate defined operation

    x ^ y = (x' v y')

• this works simply by orienting the equation into a rewrite rule
• set(auto) -> set(unfold_eq), but that might be unwise
• see Boolean algebra Sheffer base examples.