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