pub fn assoc<A: DProp, B: DProp, C: DProp>( f: Eq<Eq<A, B>, C>) -> Eq<A, Eq<B, C>>
(a = b) = c => a = (b = c).
(a = b) = c => a = (b = c)
