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