wilbowma/cur

sigma doesnt resugar properly

Opened this issue · 0 comments

run ntac/trace with this example (from here: #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)])
   ...