Example xyz (H: False): True. (* ... *)
H:False
True exact I. Qed.

Print xyz.
xyz = fun _ : False => I
     : False -> True