{-|
When defining properties, you almost always are trying to show the equivalence
of two functions. This makes that easier.
-}
λ(a : Type) →
λ(b : Type) →
λ(eq : ./Type b) →
λ(f : a → b) →
λ(g : a → b) →
λ(x : a) →
  eq.eq (f x) (g x)