Using noConfusion explicitly

Stream: lean4

[Alexandre Rademaker]

I have an MWE to show students how cases h₁ uses noConfusion to close a goal like

...
h₁ : Tree.map f (Tree.node b bl br) = Tree.nil
⊢ Tree.map f l = Tree.nil

My MWE was

example {α : Type} (a : α)
  : ∀ (t₁ t₂ : Tree α), Tree.nil = Tree.node a t₁ t₂ → False :=
  λ _ _ h => Tree.noConfusion h

But now on version 4.27.0-rc1, it is not working anymore. The error is

Type mismatch
  Tree.noConfusion ?m.12
has type
  ?m.9 ≍ ?m.11 → Tree.noConfusionType ?m.7 ?m.9 ?m.11
but is expected to have type
  False

How can I construct this Heterogeneous equality? Once more, I am just trying to illustrate how the no-confusion principle of inductive types works.

[Robin Arnez]

See lean4#11562, i.e. you need to use Tree.noConfusion rfl (eq_of_heq h) here.

[Alexandre Rademaker]

Thank you @Robin Arnez ! I used heq_of_eq instead of eq_of_heq actually.

[Robin Arnez]

Oh yeah oops