fact: Definition _FUNCTION {_4678 _4682 : Type'} := fun r : _4678 -> _4682 -> Prop => fun x : _4678 => @COND _4682 (@ex1 _4682 (r x)) (@ε _4682 (r x)) (@ε _4682 (fun z : _4682 => False)).
imports: coq theory_hol types