content: -- By Zack Grannan at https://github.com/ucsd-progsys/liquidhaskell/pull/1646
  
  {-@ LIQUID "--reflection" @-}
  {-@ LIQUID "--ple"        @-}
  {-@ LIQUID "--extensionality" @-}
  
  module ReflectClient8 where
  
  import ReflectLib8
  
  {-@ assume extensionality :: f:(a -> b) -> g:(a -> b) -> (x:a -> {f x == g x}) ->  {f == g}  @-}
  extensionality :: (a -> b) -> (a -> b) -> (a -> ()) -> ()
  extensionality _ _ _ = ()
  
  {-@ refineExt' ::
          f  : (a -> Int)
       -> g  : (a -> Int)
       -> (x : a -> { v : () | Refines (f x) (g x)})
       -> x  : a
       -> {v : () | chooseF f g x = g x}
  @-}
  refineExt' :: (a -> Int) -> (a -> Int) -> (a -> ()) -> a -> ()
  refineExt' _ _ proof x = proof x
  
  {-@ refineExt ::
          f  : (a -> Int)
       -> g  : (a -> Int)
       -> (x : a -> { v : () | Refines (f x) (g x)})
       -> {v : () | RefinesF f g}
  @-}
  refineExt :: (a -> Int) -> (a -> Int) -> (a -> ()) -> ()
  refineExt f g proof =
    extensionality (chooseF f g) g (refineExt' f g proof)
  
  {-@ predicate Refines  M1 M2 = choose   M1 M2 = M2 @-}
  {-@ predicate RefinesF F1 F2 = chooseF F1 F2 = F2 @-}
  