Lines Matching refs:f2
61 `(TypedGraphFun (t2,t3) f2) o (TypedGraphFun (t1,t2) f1) -:ens_cat U =
62 (TypedGraphFun (t4,t3) f1) o (TypedGraphFun (t1,t4) f2) -:ens_cat U` >>
65 (���x. x ��� t2 ��� f2 x ��� t3) ���
66 (���x. x ��� t1 ��� f2 x ��� t4)` by (
89 srw_tac [][Abbr`f1`,Abbr`f2`] >>
383 qmatch_abbrev_tac `(f1 o f2 -:ens_cat (homs c) = f3 o f4 -:ens_cat (homs c)) ��� X` >>
384 `IsTypedFun f2` by (
385 srw_tac [][Abbr`f2`] >>
412 `f2 ���> f1 -:ens_cat (homs c)` by (
413 fsrw_tac [][Abbr`f2`,hom_def] >>
421 `f2.dom = f4.dom` by (
422 fsrw_tac [][Abbr`f4`,Abbr`f2`,hom_def] ) >>
423 `f2.map (id f.cod -:c) = f` by (
424 srw_tac [][Abbr`f2`] >>