error when using #check with proof-term

Stream: new members

[Ayush Agrawal]

I used #print int.eq_of_sub_eq_zero and it printed the proof term:
protected theorem int.eq_of_sub_eq_zero : ∀ {a b : ℤ}, a - b = 0 → a = b :=
λ {a b : ℤ} (h : a - b = 0), have this : 0 + b = b, from (id (eq.rec (eq.refl (0 + b = b)) b.zero_add)).mpr (eq.refl b), have this : a - b + b = b, from (id (eq.rec (eq.refl (a - b + b = b)) h)).mpr this, eq.mp (eq.rec (eq.refl (a + -b + b = b)) (a.neg_add_cancel_right b)) (eq.mp (eq.rec (eq.refl (a - b + b = b)) int.sub_eq_add_neg) this)

But when I did #check λ {a b : ℤ} (h : a - b = 0), have this : 0 + b = b, from (id (eq.rec (eq.refl (0 + b = b)) b.zero_add)).mpr (eq.refl b), have this : a - b + b = b, from (id (eq.rec (eq.refl (a - b + b = b)) h)).mpr this, eq.mp (eq.rec (eq.refl (a + -b + b = b)) (a.neg_add_cancel_right b)) (eq.mp (eq.rec (eq.refl (a - b + b = b)) int.sub_eq_add_neg) this), I expected to get the type of this proof term ∀ {a b : ℤ}, a - b = 0 → a = b . But it is throwing error as attached: image.png . Can anyone help in this regard or point what am I missing? Thanks!

[Mario Carneiro]

The issue is the implicit arguments, especially in things like eq.rec. Use set_option pp.all true before the #print to get a very explicit version of the term that should be more likely to round-trip

[Ayush Agrawal]

after using set_option pp.all true above the #print, I am still having some errors:
image.png
@Mario Carneiro can you please help?