Decompose Fun_NatBijSingleton singleton case to be backend-portable

The first case of THEOREM Fun_NatBijSingleton was discharged by a single
one-liner

  BY 1..1 = {1} DEF Bijection, Surjection

which asks the default SMT pipeline to simultaneously unfold Bijection =
Injection \cap Surjection, expand the set comprehension defining
Surjection, instantiate the nested \A t \in S : \E s \in 1..1 : f[s] = t
and witness the outer \E s : S = {s}.  This worked with the bundled
provers shipped with the macOS arm64 build of TLAPS 1.6.0-pre but failed
with the Linux x86_64 build, which ships different Z3/Zenon/Isabelle
binaries and runs on a slower CI runner.  The same input file even
produced a different obligation count on the two platforms (771 vs.
732), so relying on a single SMT step for this obligation is inherently
fragile.

Rewrite the case as five small steps that any backend can close: extract
the typing and surjection facts from the definitions, derive f[1] \in S,
prove \A t \in S : t = f[1] by PICKing the (unique) index in 1..1, then
WITNESS f[1].  No backend has to invent the existential witness or
reason about set intersection at the same time as a quantified
comprehension, so the proof is robust across tlapm builds and timeout
budgets.

All 795 obligations of FunctionTheorems_proofs continue to check locally
with `tlapm --cleanfp`.

[Proofs]

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Author: lemmy

modules/FunctionTheorems_proofs.tla

@@ -879,7 +879,16 @@ THEOREM Fun_NatBijSingleton ==
   ASSUME NEW S
   PROVE  ExistsBijection(1..1,S) <=> \E s : S = {s}
 <1>1. ASSUME NEW f \in Bijection(1..1, S)  PROVE \E s : S = {s}
-  BY 1..1 = {1} DEF Bijection, Surjection
+  <2>1. f \in [1..1 -> S] /\ \A t \in S : \E i \in 1..1 : f[i] = t
+    BY DEF Bijection, Injection, Surjection
+  <2>2. f[1] \in S
+    BY <2>1
+  <2>3. \A t \in S : t = f[1]
+    <3>1. TAKE t \in S
+    <3>2. PICK i \in 1..1 : f[i] = t  BY <2>1
+    <3>. QED  BY <3>2
+  <2>. WITNESS f[1]
+  <2>. QED  BY <2>2, <2>3
 <1>2. ASSUME NEW s, S = {s}  PROVE [i \in 1..1 |-> s] \in Bijection(1..1, S)
   BY <1>2 DEF Bijection, Injection, IsInjective, Surjection
 <1>. QED  BY <1>1, <1>2 DEF ExistsBijection