Weird type coercion of Inductive types

[matzemathics]

@monsterkrampe have a look at this: (How can this possible type check?)

https://github.com/knowsys/Formale-Systeme-in-LEAN/blob/16687e35ad0ee82b61e61c96683aec5eb07e3e3d/FormalSystems/Chomsky/Regular/DFA.lean#L77-L78

where hp is defined as https://github.com/knowsys/Formale-Systeme-in-LEAN/blob/16687e35ad0ee82b61e61c96683aec5eb07e3e3d/FormalSystems/Chomsky/Regular/DFA.lean#L64

and the definition of the applied theorem is https://github.com/knowsys/Formale-Systeme-in-LEAN/blob/16687e35ad0ee82b61e61c96683aec5eb07e3e3d/FormalSystems/Chomsky/Regular/RegularGrammar.lean#L80-L82

so it is coercing the types

p.val = RegularProduction.eps v

and

p.val = RegularProduction.cons q₁ (a, q₂)

[monsterkrampe]

I'm not sure anymore but I think we resolved this (offline) at some point, right?

[matzemathics]

Yes, after it all came down to that theorem being basically a restatement of reflexivity, which is trivially handled by lean.