1 subgoal
  
  Σ : gFunctors
  heapG0 : heapG Σ
  hd, acc : val
  xs, ys : list val
  Φ : val → iPropI Σ
  ============================
  "Hxs" : is_list hd xs
  "Hys" : is_list acc ys
  "HΦ" : ∀ w : val, is_list w (reverse xs ++ ys) -∗ Φ w
  --------------------------------------∗
  WP (rev hd) acc [{ v, Φ v }]
  
1 subgoal
  
  Σ : gFunctors
  heapG0 : heapG Σ
  acc : val
  ys : list val
  Φ : val → iPropI Σ
  ============================
  "Hys" : is_list acc ys
  "HΦ" : ∀ w : val, is_list w ys -∗ Φ w
  --------------------------------------∗
  WP match: InjLV #() with
       InjL <> => acc
     | InjR "l" =>
       let: "tmp1" := Fst ! "l" in
       let: "tmp2" := Snd ! "l" in
       "l" <- ("tmp1", acc);; (rev "tmp2") (InjLV #())
     end [{ v, Φ v }]