Heterogenous Equality

Stream: new members

[Marcus Rossel]

I'm struggling with heterogenous equality. Say we have the following:

import data.vector

def n0s (n : ℕ) : vector ℕ n := vector.repeat 0 n
def p {z : ℕ} (v : vector ℕ z) : Prop := sorry
def q (a : ℕ) (b : p (n0s a)) : ℕ := sorry

theorem same (x x' : ℕ) (h : p (n0s x)) (h' : p (n0s x')) :
  x = x' → (q x h) = (q x' h') :=
  sorry

How would I prove in same that h = h'?

[Eric Wieser]

At a guess, is the proof for same intro hx, subst hx?

[Marcus Rossel]

Eric Wieser said:

At a guess, is the proof for same intro hx, subst hx?

:face_palm: yup, that worked.