# Zulip Chat Archive

## Stream: new members

### Topic: error when using #check with proof-term

#### Ayush Agrawal (Mar 23 2022 at 20:04):

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 (Mar 23 2022 at 20:48):

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 (Mar 24 2022 at 09:36):

after using `set_option pp.all true`

above the `#print`

, I am still having some errors:

image.png

@Mario Carneiro can you please help?

Last updated: Dec 20 2023 at 11:08 UTC