Functional Extensionality proof no longer works for `op_Hat_Subtraction_Greater` types without opening the module

[LukeXuan]

Consider the following fstar snippet,

module Funext

let t (k: eqtype) (v: Type) = FStar.FunctionalExtensionality.restricted_t k (fun _ -> v) 

let map_eq #k #v (m0 m1: t k v)
  : Lemma (requires forall key. m0 key == m1 key)
          (ensures m0 == m1)
  = FStar.FunctionalExtensionality.extensionality _ _ m0 m1

// open FStar.FunctionalExtensionality
let op_Hat_Subtraction_Greater = FStar.FunctionalExtensionality.op_Hat_Subtraction_Greater

let t' (k: eqtype) (v: Type) = k ^-> v 

let map_eq' #k #v (m0 m1: t' k v)
  : Lemma (requires forall key. m0 key == m1 key)
          (ensures m0 == m1)
  = FStar.FunctionalExtensionality.extensionality _ _ m0 m1

My understanding is that t and t' are exactly the same type, but map_eq is provable and map_eq' is not. Alternatively, map_eq' can also be proven if FStar.FunctionalExtensionality is opened in the module. I'm not sure if this is a bug or intentional behavior?

[mtzguido]

I think the problem is coming from #1948. Having this intermediate re-definition of ^-> is generating some different encoding of lambdas making t and t' not exactly equal... but I'm not sure why. Marking your definition unfold fixes it, as in:

unfold
let op_Hat_Subtraction_Greater = FStar.FunctionalExtensionality.op_Hat_Subtraction_Greater

You could also avoid having this definition by just opening this one symbol from the funext module:

open FStar.FunctionalExtensionality { (^->) }

[LukeXuan]

I think the problem is coming from https://github.com/FStarLang/FStar/issues/1948.

That's weird, this seems to be a problem introduced somewhere between last release (v2025.10.06) and master branch. This issue was talking about problems back in 2020. At least some other changes made recently contributes to this.