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'