;; Paulin-Mohring equality (used in coq?)
(data pm= : 2 (Π (A : (Type 0)) (Π (a : A) (Π (b : A) (Type 0))))
(pm-refl : (Π (A : (Type 0)) (Π (a : A) (pm= A a a)))))
;; pm= symmetric
(check-type
(λ [A : (Type 0)]
(λ [x : A] [y : A]
(λ [e : (pm= A x y)]
(new-elim
e
(λ [b : A]
(λ [e2 : (pm= A x b)]
(pm= A b x)))
(pm-refl A x)))))
: (Π [A : (Type 0)]
(Π [x : A] [y : A]
(→ (pm= A x y) (pm= A y x)))))
=>
core-type-error: Expected type y, but found type x while checking method for pm-refl
=>