Stream: new members
Guilherme Espada (Mar 11 2021 at 19:18):
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 (Mar 11 2021 at 19:24):
rintros ha hb rfl, contradicton
Ruben Van de Velde (Mar 11 2021 at 19:25):
intros ha hb heq, rw heq at ha, exact hb ha,
Guilherme Espada (Mar 11 2021 at 19:33):
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 (Mar 11 2021 at 19:34):
It rewrites with
Ruben Van de Velde (Mar 11 2021 at 19:36):
Try now - I was rewriting in the wrong direction.
rintro rfl does
intro heq, subst a
Guilherme Espada (Mar 11 2021 at 19:41):
Thank you! now I understand it!
Marcus Rossel (Mar 12 2021 at 09:25):
Last updated: May 08 2021 at 04:14 UTC