Automate elimination of on l _; treat on specially in matching, inheriting the match keys of its second argument

Author: nikswamy

lib/pulse/lib/Pulse.Lib.Inv.fst

@@ -60,13 +60,15 @@ ghost fn move i p l1 l2
         ensures on l' p
       {
         bwd ();
+        rewrite on l1 p as on l_ p;
         let f = f; f ()
       };
       ghost fn g' ()
         requires on l' p
         ensures on l2 p
       {
         let g = g; g ();
+        rewrite on l_ p as on l1 p;
         fwd ();
       };
       fold move_tag l2 l' p f' g';