Function prop::eq::assoc_right

source ·
pub fn assoc_right<A: DProp, B: DProp, C: DProp>(
    (f0, f1): Eq<Eq<A, B>, C>
) -> Imply<A, Eq<B, C>>
Expand description

(a == b) == c => a => (b == c)