Jeremy Dawson

2018-11-13 03:22:30 UTC

Hi coq-club,

Having made a definition f x y z = a b c

how do I get this as an equality theorem that can be used to rewrite

a b c to f x y z?

(I realise I can set it out as a lemma and prove it using unfold, but

I'm assuming it's already there as a theorem that I just need to find

out how to get hold of it)

thanks

Jeremy

Having made a definition f x y z = a b c

how do I get this as an equality theorem that can be used to rewrite

a b c to f x y z?

(I realise I can set it out as a lemma and prove it using unfold, but

I'm assuming it's already there as a theorem that I just need to find

out how to get hold of it)

thanks

Jeremy