proposition: Lemma _FUNCTION_def {_4678 _4682 : Type'} : (@_FUNCTION _4678 _4682) = (fun r : _4678 -> _4682 -> Prop => fun x : _4678 => @COND _4682 (@ex1 _4682 (r x)) (@ε _4682 (r x)) (@ε _4682 (fun z : _4682 => False))).
proof: Proof. exact (eq_refl (@_FUNCTION _4678 _4682)). Qed.
imports: coq theory_hol types