theorems for free, polymorphic equality

[sassa_nf]

Can someone walk me through the first paragraph of the section on polymorphic equality?
The programming language Miranda provides a polymorphic equality function, with type:

(=): ∀ X, X → X → Bool
Applying parametricity to the type of (=) yields, for all a : A → A'
for all x, y ∈ A, (x =A y) = (a x =A' a y).This is obviously falseThen they also say

Comments

[ex_juan_gan]

Is it

for all a : A → A' for all x, y ∈ A, (x =A y) = (a x =A' a y)

?

Anyway, looks totally weird to me.

But I don't believe in parametricity theorem anyway.

[sassa_nf]

Yes, it is "for all a", at the end of the line above the statement. I was just copying the article.