FCP_ss : ssfrag
simpLib.SSFRAG{ac = [], congs = [], convs = [], dprocs = [], filter = NONE, rewrs = [|- !i. i < dimindex (:'b) ==> ($FCP g ' i = g i), |- !g. (FCP i. g ' i) = g, |- !x y. (x = y) = !i. i < dimindex (:'b) ==> (x ' i = y ' i)]} : ssfrag