fact: Definition _SEQPATTERN {_4611 _4614 : Type'} := fun r : _4614 -> _4611 -> Prop => fun s : _4614 -> _4611 -> Prop => fun x : _4614 => @COND (_4611 -> Prop) (exists y : _4611, r x y) (r x) (s x).
imports: coq theory_hol types