Original proof in the cited forall x natural-deduction system
Goal: from forall x(Px->Qx) and forall x Px, derive forall x Qx
1. forall x(Px->Qx)       Premise
2. forall x Px           Premise
3. Pc->Qc                forall E, 1; c chosen fresh
4. Pc                    forall E, 2
5. Qc                    ->E, 3,4
6. forall x Qx           forall I, 5
Freshness: c occurs in neither undischarged premise and there are no additional open assumptions. Replace the whole occurrence of c in Qc.
Countermodel to Fa -> forall x Fx: D={A,B}, a denotes A, F={A}. Fa true, forall x Fx false.