theory Test
  imports Main
begin
  
lemma fixes x :: int 
  shows "x > 0 \<Longrightarrow> x * x > 0" 
  by simp
    
lemma "\<exists> x. drinks x \<longrightarrow> (\<forall> y. drinks y)" 
  by blast 
    
lemma "(\<exists> x. P x) = (\<forall> x. P x)" 
  by auto
    
end