
However, for any particular \(F\)  with a given proof term \(M\)  of \(\forall _{f}\big (\forall _{n\in }(fn\in )\rightarrow Ff\in \big )\) , its extracted term \(et(M)\)  (see [1]}, section 7.2.5) is continuous, which is enough to prove the strong extensionality of \(F\) .

