heq_comm

Stream: Is there code for X?

[Violeta Hernández]

Are we really missing this?

theorem heq_comm.{u} {α β : Sort u} (a : α) (b : β) : HEq a b ↔ HEq b a := by
  constructor <;> rintro ⟨⟩ <;> rfl

[Adam Topaz]

do you really need an iff version, or can you get by with docs#HEq.symm ?

[Violeta Hernández]

Actually, symm does work for my purposes

[Kyle Miller]

Maybe we'll have it soon: lean4#5456

[Violeta Hernández]

Thanks!