proposition: Lemma _SEQPATTERN_def {_4611 _4614 : Type'} : (@_SEQPATTERN _4611 _4614) = (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)).
proof: Proof. exact (eq_refl (@_SEQPATTERN _4611 _4614)). Qed.
imports: coq theory_hol types