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