Open RobertoZunino opened 9 years ago
Require Import HoTT. Goal True. Proof. assert {m:nat & True} as n. exists 0. exact tt. transparent assert (H: True). destruct n. (* Anomaly: variable n unbound. Please report. *)
Using assert instead works fine.
assert
Using
assert
instead works fine.