theorem lfneq1d (_G: wff) (_F1 _F2: set) (n: nat): $ _G -> _F1 == _F2 $ > $ _G -> lfn _F1 n = lfn _F2 n $;
_G -> _F1 == _F2
_G -> n = n
_G -> lfn _F1 n = lfn _F2 n