Lines Matching refs:f2
194 ``!f1 f2 al. INJ f1 (set (MAP FST al)) UNIV ==>
195 (alist_to_fmap (MAP (\ (x,y). (f1 x, f2 y)) al) =
196 MAP_KEYS f1 (f2 o_f alist_to_fmap al))``,
238 Q.MATCH_ABBREV_TAC `MAP f2 al = al` THEN
239 Q_TAC SUFF_TAC `!x. MEM x al ==> (f1 x = f2 x)` THEN1 PROVE_TAC[MAP_EQ_f] THEN
240 SRW_TAC[][Abbr`f1`,Abbr`f2`] THEN
325 qmatch_abbrev_tac `ALL_DISTINCT (MAP f2 ls)` >>
326 qsuff_tac `MAP f2 ls = MAP f1 ls` >- rw[] >>
327 rw[MAP_EQ_f,Abbr`f1`,Abbr`f2`,Abbr`ls`,DOMSUB_FAPPLY_THM])
332 ``!f1 f2. (fmap_to_alist f1 = fmap_to_alist f2) ==> (f1 = f2)``,
354 qmatch_assum_abbrev_tac `MAP f1 ls = MAP f2 ls` >>
356 qsuff_tac `(MAP f3 ls = MAP f1 ls) /\ (MAP f4 ls = MAP f2 ls)` >- rw[] >>
357 rw[MAP_EQ_f,Abbr`f1`,Abbr`f2`,Abbr`f3`,Abbr`f4`,Abbr`ls`,DOMSUB_FAPPLY_THM])
457 ``!f1 f2 al mal v. INJ f1 (set (MAP FST al)) UNIV /\
458 (mal = MAP (\(x,y). (f1 x,f2 y)) al) /\
459 (v = MAP_KEYS f1 (f2 o_f alist_to_fmap al)) ==>