(* -------------------------------------------------------------------- *)
require import AllCore.

(* -------------------------------------------------------------------- *)
lemma L (p q : bool) : p => q.
proof.
move=> h.
fail apply: h.
abort.