finish

Stream: new members

[Michael Beeson]

An observation: ifinish cannot prove this:

h41: t ∈ a → t ∈ x ∨ ¬t ∈ x
h40: t ∈ x → t ∈ a
⊢ t ∈ a ↔ t ∈ x ∨ t ∈ a ∧ ¬t ∈ x

but if I manually do one 'split', then ifinish can do both the two new goals.