Prove that universal and existential quantifier become one for higher dimensional truth values

[bvssvni]

Sketch proof:

∀ f : I -> I -> I {
    ∀ a : I { lift(
        (∀ p : (I ~= I) { lift(f(p, p)) } : un(a ~= a)) ==
        (∃ p : (I ~= I) { lift(f(p, p)) } : nu(a ~= a))
    ) } : un(1)
}

The idea is that since there is no false analogue for higher dimensional truth values,
the universal and existential quantifier behave the same,
except un is nu.