Lines Matching refs:f2
15 `Seq (f1:'a->'b) (f2:'b->'c) = \x. f2(f1 x)`;
19 `Par f1 f2 = \x. (f1 x, f2 x)`;
23 `Ite f1 f2 f3 = \x. if f1 x then f2 x else f3 x`;
27 `Rec (x:'a) = if f1 x then f2 x else Rec (f3 x)`;
304 ``!f f1 f2 f3.
305 (!x:'a. f x = if f1(x) then f2(x) else f(f3 x))
307 ==> (f:'a->'b = Rec f1 f2 f3)``,
329 METIS_PROVE [] ``!f M. (let f2 = f in f2 M) = f M``);