Proving equality of Decidable instances for propeq types

Stream: lean4

[Markus Schmaus]

Here is a #mwe:

import Mathlib.Tactic

def Foo (x : Bool): Prop := x = true

def Foo' (x : Bool): Prop := x ≠ false

theorem Foo_eq_Foo' (x : Bool) : Foo x = Foo' x := by
  simp only [Foo, Foo', ne_eq, Bool.not_eq_false]

instance inst (x : Bool) : Decidable (Foo x) :=
  if h : x then isTrue h
  else isFalse h

instance inst' (x : Bool) : Decidable (Foo' x) :=
  if h : x then isTrue <| by
    simp only [Foo', h, ne_eq, not_false_eq_true]
  else isFalse <| by
    simp only [Foo', h, ne_eq, not_true_eq_false, not_false_eq_true]

theorem decidable_eq_decidable' : Decidable (Foo x) = Decidable (Foo' x) := by
  simp only [Foo_eq_Foo']

theorem inst_eq_inst' (x : Bool) : HEq (inst x) (inst' x) := by
  sorry

I have two types which are provably equal, like Foo and Foo' in the example, and two Decidable instances that are extensionally equivalent. Is it somehow possible to prove that they are the same?

[Junyan Xu]

theorem inst_eq_inst' (x : Bool) : HEq (inst x) (inst' x) :=
  Subsingleton.helim decidable_eq_decidable' _ _