pub fn assoc_right<A: DProp, B: DProp, C: DProp>( (f0, f1): Eq<Eq<A, B>, C>) -> Imply<A, Eq<B, C>>
(a = b) = c => a => (b = c)
