?2) cosa "corrisponde" alla simplify? multivm/breakpoint
=> la mu (+ iota) normalize
3) nelim bacata (assert ...), ma napply funziona
prod_lemmas/symmetric_eqquadruple, napply (Prod4T ...)
*4) nrewrite bacata, ma napply funziona
?2) cosa "corrisponde" alla simplify? multivm/breakpoint
=> la mu (+ iota) normalize
3) nelim bacata (assert ...), ma napply funziona
prod_lemmas/symmetric_eqquadruple, napply (Prod4T ...)
*4) nrewrite bacata, ma napply funziona