def foo : Prop :=
((λ (a : ℕ), a) = λ (a : ℕ), a) ↔ true