Straightline matches with different cases but it makes less sense

[dayeol]

Sam and I have debugged together and the straightline is somehow working in an unexpected way.
While I was trying to write a lemma that works for any i : Z in general,
presence of a hypothesis we put makes straightline behave differently while going through the proof.
Basically, Hi below is irrelevant but somehow it makes the proof go through
while removing it makes it get stuck.

  Lemma read_flag_from_status                                                                                                                                                                                 
    (functions : list (string * (list string * list string * Syntax.cmd)))                                                                                                                                 
    (H : spec_of_abs_mmio_read32 functions)                                                                                                                                                                 
    (tr : trace)                                                                                                                                                                                             
    (m : mem)                                                                                                                                                                                                
    (R : mem -> Prop)                                                                                                                                                                            
    (s : state)                                                                                                                                                                                   
    (H0 : R m)                                                                                                                                                                                     
    (H1 : execution tr s)                                                         
    (i : Z)                                                                                  
    (* Hi needs to go away once the issue *)                                       
    (Hi : i <= i) :                                                              
    call functions AbsMMIO.abs_mmio_read32 tr m [word.of_Z AES_STATUS0]        
      (fun (t : trace) (m0 : mem) (rets : list Semantics.word) =>                   
       exists l : locals,                                                     
         map.putmany_of_list_zip ["status"] rets map.empty = Some l /\          
         cmd (call functions)                                                     
           (cmd.set "out"                                                      
              (expr.op bopname.and "status"                               
                 (expr.op bopname.slu 1 AES_STATUS_INPUT_READY))) t m0 l      
           (fun (t0 : trace) (m1 : mem) (l0 : locals) =>                        
            list_map (get l0) ["out"]                                         
              (fun rets0 : list Semantics.word =>                                   
               exists (status out : Semantics.word) (s' : state),            
                 execution t0 s' /\                                            
                 read_step s STATUS status s' /\                                              
                 R m1 /\                                                       
                 rets0 = [out] /\                                          
                 word.eqb out (word.of_Z 0) =                                      
                 negb (is_flag_set status AES_STATUS_INPUT_READY)))).  

I have passed the branch to Sam and he will follow up with the issue.
https://github.com/dayeol/silveroak/tree/debug-straightline-diverge