cur
cur copied to clipboard
sigma doesnt resugar properly
run ntac/trace
with this example (from here: https://github.com/wilbowma/cur/issues/121)
(ntac/trace
(∀
(T : Type)
(Σ (lst : (List T)) (And (== (List T) lst (nil T)) (Not (== (List T) lst (nil T)))))
False)
(by-intros T ex)
(by-destruct ex #:as [(b H)])
...