pub fn assoc<A: Prop, B: Prop, C: Prop>( ((x0, x1), x2): And<And<A, B>, C>) -> And<A, And<B, C>>
(a ∧ b) ∧ c => a ∧ (b ∧ c).
(a ∧ b) ∧ c => a ∧ (b ∧ c)
