Nontrivial HEq

Stream: lean4

[Marcus Rossel]

I've asked in a previous thread how to prove a simple heterogeneous equality. Unfortunately that didn't work for my real project, so I've come up with a more complex MWE:

def Graph            : Type                                  := sorry
def Path (g : Graph) : Type                                  := sorry
def Path.final       : Path g → Type                         := sorry
def Path.NonEmpty    : Path g → Prop                         := sorry
def Path.SamePrefix  : Path g → Path g → Prop                := sorry
def Path.final'      : (p : Path g) → Path.NonEmpty p → Type := sorry

def Sibling (p : Path g) := { p' : Path g // Path.SamePrefix p p' }
structure Leaf (g : Graph) where path : Path g

example (g : Graph) (l : Leaf g) (s : Sibling l.path) (f : s.val.final) (hn : Path.NonEmpty s.val) (hf : s.val.final = s.val.final' hn) : HEq f (hf ▸ f) := by
  sorry

Again the goal is in a sense trivial as it feels intuitively obvious that a type cast should produce something heterogeneously equal (perhaps my intuition fails me here?). But I don't know how to solve this proof.
Any guidance on how to approach this would be appreciated :)

[Kyle Miller]

This is docs4#cast_heq

[Kyle Miller]

example (g : Graph) (l : Leaf g) (s : Sibling l.path) (f : s.val.final) (hn : Path.NonEmpty s.val) (hf : s.val.final = s.val.final' hn) :
  HEq f (hf ▸ f) :=
(cast_heq _ _).symm

[Marcus Rossel]

Hmm, this still doesn't work for my real project. I'll try to refine the MWE.