Lines Matching refs:f2
612 `���f1 f2 n. is_nat_trans n ��� is_functor f1 ��� is_functor f2 ��� (f1 ���> f2) ��� (f1.dom = ntcod n) ���
613 (functor_nt (f2 ��� f1) n = functor_nt f2 (functor_nt f1 n))`,
773 qmatch_abbrev_tac `g##(g1 o f1 -:g.dom) = g##(g2 o f2 -:g.dom)` >>
779 `f2 ���> g2 -:g.dom` by (
781 srw_tac [][Abbr`f2`,Abbr`g2`] >>
785 qspecl_then [`g`,`g.dom`,`g.cod`,`f2`,`g2`] mp_tac morf_comp >>
788 `g##f2 = h@+x` by metis_tac [] >>