Skip to main content

norm1_comp

prop::fun

Function norm1_comp 

Source 
pub fn norm1_comp<F: Prop, G1: Prop, G2: Prop, G3: Prop, G4: Prop>() -> Eq<Norm1<Norm1<F, G1, G2>, G3, G4>, Norm1<F, Comp<G3, G1>, Comp<G4, G2>>>
Expand description

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