dom (IncAddr (F,k)) = dom F by Def40;
hence not IncAddr (F,k) is empty ; :: thesis: verum