a ∈ tt_ctx → b ∉ tt_ctx → a ≠ b

Stream: new members

[Guilherme Espada]

Where tt_ctx is a finmap.

I'm guessing this is done with congruence, however, I don't know the exact procedure to solve this, and library_search doesn't find anything (maybe I'm stating it wrong?)

[Ruben Van de Velde]

rintros ha hb rfl, contradicton

[Ruben Van de Velde]

Or longer, intros ha hb heq, rw heq at ha, exact hb ha,

[Guilherme Espada]

First version works, but what does the rfl at the end do?
(the second version doesn't seem to work on my end)

[Eric Wieser]

It rewrites with a=b

[Ruben Van de Velde]

Try now - I was rewriting in the wrong direction. rintro rfl does intro heq, subst a

[Guilherme Espada]

Thank you! now I understand it!

[Marcus Rossel]

ne_of_mem_of_not_mem