pub fn in_left_arg<A: Prop, B: Prop, C: Prop>( f: Eq<A, B>, g: Eq<A, C> ) -> Eq<C, B>
(a == b) ∧ (a == c) => (c == b)