pub fn distrib<A: Prop, B: Prop, C: Prop>( x: Or<And<A, B>, And<A, C>>) -> And<A, Or<B, C>>
(a ∧ b) ∨ (a ∧ c) => a ∧ (b ∨ c)