Heterogeneous equality with coercion

Stream: new members

[Ryan Whitty]

Hi! I'm trying to finish a lemma of heterogeneous equality, and I've gotten to where the goal is:

HEq (Sigma.snd a x) ↑(Sigma.snd a x)

The proof containing this is probably to long to post in full, but the necessary info is that (Sigma.snd a) is a function with range { x // x ∈ α_nonzero }, and the second term in the goal is being coerced to type α. α here is a finite alphabet, and α_nonzero is α without its 0 element.

Is there a nice way to show that two objects that are identical up to coercion are heterogeneously equal? Thanks!

[Ruben Van de Velde]

I'm not sure that's true. Question is, how did you get here and can you back out to a point where you're not dealing with HEq?

[Ryan Whitty]

Thanks for the quick response! I'm not sure I can avoid using HEq, since the things I'm trying to show equality with originally have different types. What are you not sure is true?

[Daniel Weber]

Note that HEq also implies that the types are equal. Could you send a #mwe of where you need the heterogeneous equality?

[Ruben Van de Velde]

extract_goal might help if it doesn't get confused by coercions