Socrates

procedure Main with SPARK_Mode is

   type Domain is new Integer with Ghost;

   Socrates : constant Domain := 0 with Ghost;

   function Human (X : Domain) return Boolean
     with Ghost, Import;

   function Mortal (X : Domain) return Boolean
     with Ghost, Import;

begin
   pragma Assume (Human (Socrates));
   pragma Assume (for all X in Domain => (if Human (X) then Mortal (X)));

   pragma Assert (Mortal (Socrates));
end Main;