1 2 3 4 5 6 7 8
(* To shorten interactive scripts, it is better that Try catches non-existent names in Unfold [cf BZ#263] *) Lemma lem1 : True. try unfold i_dont_exist. trivial. Qed.