lapply (FmP ????? a) as H1; lapply (FmP ????? a') as H2;
cut (REW ????? (map_arrows2 ?? F ?? (ℳ_1 a)) =
REW ????? (map_arrows2 ?? F ?? (ℳ_1 a')));[2:
lapply (FmP ????? a) as H1; lapply (FmP ????? a') as H2;
cut (REW ????? (map_arrows2 ?? F ?? (ℳ_1 a)) =
REW ????? (map_arrows2 ?? F ?? (ℳ_1 a')));[2: