Consider more automation with conjunctions

[wdcraft01]

For discussion/consideration. Low priority. Working in the logic/set_theory/enumeration context on enumerated sets and the Set.deduceEnumProperSubset() method, I discovered the following interesting example. Prove-It was able to automatically deduce that:

{2 ∉ {1, a}} ⊢ 2 ∉ {1, a, 1}

but was NOT able to deduce that:

{2 ∉ {1, a, 1}} ⊢ 2 ∉ {1, a}

The error message included the following:

Proof step failed assuming {2 not-in {1 , a , 1}}: Unmet specialization requirement: (2 != 1) and (2 != a) when specializing |- forall_{l in Naturals} [forall_{x, y_1,...,y_l | (x != y_1) and ... and (x != y_l)} (x not-in {y_1 , ... , y_l})] with {l: 2, x: 2, y: (1 , a)}

which hints at the possibility that in the 2nd case above we might be failing because Prove-It is looking for a binary conjunction of the form (2!=1)∧(2!=a), but would have found a triplet of the form (2!=1)∧(2!=a)∧(2!=1) instead and not “seen” that the desired conjunction was contained there. That example suggests it might be worth considering somewhat more elaborate automation/processing of conjunctions to allow more automatic use of the individual operands.

[wdcraft01]

Here is what appears to be a related example. In working in the settheory/containment/_demonstrations\.ipynb, I had established the following (as a simple demonstration exercise):

x_in_Y_kt = {x ∈ X, X ⊂ Y} ⊢ x ∈ Y

then used x_in_Y_kt.asImplication(hypothesis=Subset(X, Y)) and x_in_Y_kt.asImplication(hypothesis=InSet(x, X)) to produce the following (respectively):

{x ∈ X} ⊢ (X ⊂ Y) ⇒ x ∈ Y {X ⊂ Y} ⊢ (x ∈ X) ⇒ x ∈ Y

but trying to use x_in_Y_kt.asImplication(hypothesis=And(InSet(x, X), Subset(X, Y))) produced

{x ∈ X, X ⊂ Y} ⊢ (x ∈ X ∧ X ⊂ Y) ⇒ x ∈ Y

without eliminating the assumptions on the lhs of the turnstile. The result resists various efforts to use the hypothesis argument in different ways. For example, this also fails to eliminate the assumptions: x_in_Y_kt.asImplication(hypothesis=x_in_Y_kt.assumptions)