#410 More automatic proofs about finiteness

[Guillaume Verdier]

Currently, the auto prover is able to prove some very simple goals about finiteness with the class FiniteInclusionTac. For example, if A ⊆ B and finite(B), it proves finite(A).
This class could be extended to prove more cases such as:

• finite(A) |- finite(A \ B)
• finite(A), finite(B) |- finite(A ∪ B)
• finite(A) |- finite(A ∩ B) and finite(B) |- finite(A ∩ B)

[Guillaume Verdier]

These cases have been implemented and merged in commit [3fc052].