Replace turnstyle ⊢ by something more student friendly

[jnarboux]

The separation between hypothesis and what needs to be proved: ⊢ could be replaced.

XYZ: Type
AA': Set X
f: X → Y
g: Y → Z
BB': Set Y
x: X
x_mem: x ∈ f ⁻¹' (B ∪ B')
⊢ x ∈ f ⁻¹' B ∪ f ⁻¹' B'

Could be displayed in a more user friendly manner, something like (with a translation in the french version):
The word goal should be kept for denoting the pair (hypotheses, conclusion), so it should be avoided to denote what needs to be proved.

---

Hypothesis:
XYZ: Type
AA': Set X
f: X → Y
g: Y → Z
BB': Set Y
x: X
x_mem: x ∈ f ⁻¹' (B ∪ B')

---

We need to prove that:
x ∈ f ⁻¹' B ∪ f ⁻¹' B'