Discharging impossible branches for non-injective-function reasoning

Preamble: this is a blocker in KPlutus and may also be a blocker for any development that deals with equality and non-injective functions.

Consider the following function:

syntax Value ::= CanonicalRational(Int, Int) [function, total]

and the following two specifications for a function that reasons about the equality of canonical rationals (CRs):

claim
  <k>
    F_EQ_RATIONAL_CORE => gLookup(k_True) ...
  </k>
  <env>
    k_w1 |-> CanonicalRational(AN:Int, AD:Int)
    k_w2 |-> CanonicalRational(BN:Int, BD:Int)
      =>
    .Map
  </env>
  requires CanonicalRational(AN:Int, AD:Int) ==K CanonicalRational(BN:Int, BD:Int)

  claim
  <k>
    F_EQ_RATIONAL_CORE => gLookup(k_False) ...
  </k>
  <env>
    k_w1 |-> CanonicalRational(AN:Int, AD:Int)
    k_w2 |-> CanonicalRational(BN:Int, BD:Int)
      =>
    .Map
  </env>
  requires CanonicalRational(AN:Int, AD:Int) =/=K CanonicalRational(BN:Int, BD:Int)

which fully cover the space of possibilities, in that two CRs are either equal or not equal. When these specifications are to be used, however, for example, in the following configuration:

<generatedTop>
    <k>
      F_EQ_RATIONAL_CORE ~> [ SOME FRAME ]
    </k>
    <env>
      k_w1 |-> CanonicalRational ( ONUMX:Int , ODENX:Int )
      k_w2 |-> CanonicalRational ( ONUM:Int , ODEN:Int )
    </env>
    [ REST OF CONFIGURATION ]
  </generatedTop>

a third case appears, with this constraint:

#Not ( #Exists AD:Int . #Exists AN:Int . #Exists BD:Int . #Exists BN:Int . 
    #Not ( { CanonicalRational ( AN:Int , AD:Int ) #Equals CanonicalRational ( BN:Int , BD:Int )  } ) #And 
    { CanonicalRational ( AN:Int , AD:Int ) #Equals CanonicalRational ( ONUMX:Int , ODENX:Int ) } #And 
    { CanonicalRational ( BN:Int , BD:Int ) #Equals CanonicalRational ( ONUM:Int , ODEN:Int ) } 
)
    #And
#Not ( #Exists AD:Int . #Exists AN:Int . #Exists BD:Int . #Exists BN:Int . 
    { CanonicalRational ( AN:Int , AD:Int ) #Equals CanonicalRational ( BN:Int , BD:Int ) }   #And 
    { CanonicalRational ( AN:Int , AD:Int ) #Equals CanonicalRational ( ONUMX:Int , ODENX:Int ) }  #And 
    { CanonicalRational ( BN:Int , BD:Int ) #Equals CanonicalRational ( ONUM:Int , ODEN:Int ) } 
)

and I am not sure why the SMT solver does not find the trivial instantiation that falsifies the second #Not. On top of this, if a function is partial (which CanonicalRational should be but is not so that the proofs can go through), this gets more complex with #Ceils floating around, but still the same trivial instantiation works.

Start with the KPlutus equality claims for CanonicalRational and reproduce them using the shown generatedTop configuration and SMT constraint. Trace why the second #Not is not discharged; done means the solver handles the trivial instantiation or the issue documents a confirmed limitation and its required change.