card (FreeGen p) c= 2 |^ p by LmX;
hence FreeGen p is finite ; :: thesis: verum