theorem lfnauxeq2 (F: set) (_k1 _k2 n: nat): $ _k1 = _k2 -> lfnaux F _k1 n = lfnaux F _k2 n $;
_k1 = _k2 -> _k1 = _k2
_k1 = _k2 -> lfnaux F _k1 n = lfnaux F _k2 n