Is it normal / expected that I need the
? for this to succeed? If I remove it, it fails with "Not evar". I wonder what's the use case for this tactic if this behavior is expected.
Goal True. evar (P: Prop). is_evar P.
Last updated: Feb 09 2023 at 00:03 UTC