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)