pub fn in_left_arg<A: Prop, B: Prop, C: Prop>( (x, y): And<A, B>, g: Imply<A, C>) -> And<C, B>
(a ∧ b) ∧ (a => c) => (c ∧ b).
(a ∧ b) ∧ (a => c) => (c ∧ b)