We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Revert bad change, it's indeed restricted functional extensionality indeed provable
Updated SMT Equality and Extensionality in F* (markdown)
Extensionality is not provable in F*, even in restricted form, it's still an axiom