First? order logic forall shifting laws

[eviefp]

Does any of this make sense? It seems weird/trivial.

module Main where

import Data.Either (Either)
import Data.Tuple (Tuple)


-- (∀x. a → x) ⇔ a → (∀x. x)
one ∷ ∀ a
    . (∀ x. a → x)
    → (a → (∀ x. x))
one f = f

-- (∀x. a ∧ x) ⇔ a ∧ (∀x. x)
two ∷ ∀ a
    . (∀ x. a → x → Tuple a x)
    → (a → (∀ x. x → Tuple a x))
two f = f

-- (∀x. a ∨ x) ⇔ a ∨ (∀x. x)
three ∷ ∀ a
      . (∀ x. (a → Either a x) → (x → Either a x) →  Either a x)
      → ( (∀ x. a → Either a x) → (∀ x. (x → Either a x) → Either a x) )
three f = f