Interpretation of Partial Functions from Z to Isabelle/HOL

Question

I am trying to write a predicate such that, "if a certain constant is true"(in this case if 'sec=ok') then the predicate will evaluate to False, because I've written an expression in the consequent of that particular implication that contradicts with another expression elsewhere in the predicate. (f%^x ≠ g%^x) ∧ (f%^ci = g%^ci) should contradict, given the fact that both x and ci are universally quantified and have the same type.

However, Nitpick produces a counter example that I am not able to understand. I was hoping if someone could kindly check this lemma and see whether a contradiction can be proved. Or else let me know where I'm going wrong. So a brief description is as follows;

• f and g are two partial functions from arbitrary types 'a to 'b.

• 'sec' is a constant with values 'ok' and 'notok'

  f::'a-|->'b
  g::'a-|->'b
  
  lemma simpleExample: 
  shows "∀ (ci::'a ) (a::'a set) (b::'b set) ( f::'a  <=> 'b) . f ∈ (a-|-> b) ∧ card f > 0 -->       
      (∃  ( g::'a  <=> 'b) . g ∈ (a-|->b) ∧ a=(dom f ∪ dom g) ∧
      (  ∀ (x ::'a) . sec=ok --> f%^x ≠ g%^x) ∧  f%^ci = g%^ci )  "
  

I've also seen a 'subtle' difference between two Z Math toolkits regarding Function Application. I've tried both but the problem remains.

    In HIVE Z Math toolkit :  "R %^ x      == The(λy. (x,y) : R )  "
    In HOL-Z Math Toolkit :   "R %^ x      == (@y. (x,y) : R)"

The Nitpick error can be seen here http://i58.tinypic.com/316te1t.png

NOTE: For reference, please find the definition of partial function I'm using currently from HOL-Z.

     type_synonym  ('a,'b) lts = "('a*'b) set"     (infixr "<=>" 20)

     prodZ         ::"['a set,'b set] => ('a <=> 'b) " ("_ %x _"  [81,80] 80)

     "a %x b"      == "a <*> b"

     rel           ::"['a set, 'b set] => ('a <=> 'b) set"  ("_ <--> _"   [54,53] 53)
     rel_def       : "A <--> B    == Pow (A %x B)"

     partial_func  ::"['a set,'b set] => ('a <=> 'b) set"   ("_ -|-> _"   [54,53] 53)
     partial_func_def  : "S -|-> R    == 
          {f. f:(S <--> R) & (! x y1 y2. (x,y1):f & (x,y2):f  --> (y1=y2))}"

     rel_appl      :: "['a<=>'b,'a] => 'b"    ("_ %^ _"  [90,91] 90)
     rel_appl_def  :  "R %^ x       == The(λy. (x,y) : R)"