Hi ! How can I discriminate equalities like
Heq_l : Nnil ~= Ncons x l
Ncons are dependent list constructors ?
I think this is the one, in
Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).
one way to work with assumptions that use
JMeq is to apply
JMeq_eq (uses axiom
Eqdep.Eq_rect_eq.eq_rect_eq on recent Coq), then they become a normal equality.
It seems not sufficient in this case because both sides don't have the same type for
JMeq_eq to be applicable.
Last updated: Dec 06 2023 at 15:01 UTC