``` coq 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.