src/HOLCF/Bifinite.thy

 apply (rule lessI)
 done
 
 lemma finite_deflation_lift_approx: "finite_deflation (lift_approx i)"
 proof
-  fix x
+  fix x :: "'a lift"
   show "lift_approx i\<cdot>x \<sqsubseteq> x"
     unfolding lift_approx_def
     by (cases x, simp, simp)
   show "lift_approx i\<cdot>(lift_approx i\<cdot>x) = lift_approx i\<cdot>x"
     unfolding lift_approx_def