pub fn eq_left_false<A: Prop, B: Prop, C: Prop>( nc: Not<C> ) -> Eq<And<A, C>, And<B, C>>
¬c => (a ∧ c) == (b ∧ c).
¬c => (a ∧ c) == (b ∧ c)