How to parse this example?

Stream: maths

[None proffered]

How to parse this example?

[None proffered]

example : (∃ x, p x → r) ↔ (∀ x, p x) → r

[None proffered]

(deleted)

[None proffered]

Is it (1) [(∃ x, p x → r)] ↔[ (∀ x, p x) → r] for CCCC CCCC TNTN TTTT in M8/VL4; or
Is it (2) [(∃ x, p x → r) ↔ (∀ x, p x)] → r for CCCC TTTT TNTN TTTT in M8/VL4.
In either case, Eqs. 1 or 2 are not tautologous (all designated proof value of T).

[Kevin Buzzard]

variables (α : Type) (p : α → Prop) (r : Prop)
example : ( (∃ x, p x → r) ↔ (∀ x, p x) → r ) = ( (∃ x, p x → r) ↔ ( (∀ x, p x) → r ) ) := rfl

Apparently it's the former: (1).

[Mario Carneiro]

@None proffered the parse is (1) as Kevin says. I don't know what "CCCC CCCC TNTN TTTT" means; what is M8/VL4? This theorem is not true when the domain of x is empty. I assume you got this example from tests/finish3.lean, which proves two versions of this:

variables (A : Type) (p : A → Prop) (r : Prop)
example (a : A) : (∃ x, p x → r) ↔ (∀ x, p x) → r := begin safe [iff_def]; exact h a end
example : (∃ x, p x → r) → (∀ x, p x) → r := by finish

So it is provable in one direction unconditionally, but the bidirectional version requires some a : A, i.e. A has to be nonempty.