update proof of fo_pat_correct

(and fix error in definition of fo_pat)