Function norm2_def 

pub fn norm2_def<F: Prop, G1: Prop, G2: Prop, G3: Prop>() -> Eq<Norm2<F, G1, G2, G3>, Comp<Comp<G3, F>, ParInv<G1, G2>>>

f[g1 x g2 -> g3] == (g3 . f) . (inv(g1) x inv(g2)).