Leibniz and ToBoolean Operators and Proof Fragment

[belout...@xxxxxxxxx]

Hi all,
Somme questions concerning technical concepts in the " TLA+2 A Preliminary Guide-January 2014".

1)- Section 5.2, page7, says that the reasonable theorem of the module M is not valid in TLA+1. I think that the theorem is always valid, because the problem is with the INSTANTIATION. With instantiation meaning a kind of substitution, the given INSTANCE statement " INSTANCE M with C <- x, D <- y, F <- Prime " substitutes VARIABLES for CONSTANTS, where these two concepts come from different semantics levels in TLA theory. The theorem remain valid if we have substitute CONSTANTs for CONSTANTs. For example, with the following substitution(instantiation)  .... with C <- Cst1, D <- Cst2, ...,  where Cst1 and Cst2 are Constants, the following is true :
           THEOREM  Cst1 = Cst2 ==> Cst1' = Cst2'

2)- At the bottom of subsubsection 7.8.2, page 34, we have a proof fragment that I think is about the following theorem : 
                                       THEOREM  x > 3 ==> x > 2
The below proof fragment is said to be correct because .....
    <3>2  x > 3        
    <3>3  x > 2
          By <3>2  

I think that this proof fragment misses some fundamental facts that allow us to formally derive x > 2 from x > 3.
Our suggestions to complete the fragment correctness are the following steps :

    The fact that 3 > 2 is true By Definition of > On Integer or Real
     And
    The fact that the Relation > is transitive.

3)- section 8, page 36, gives a recursive definition for the Operator ToBoolean, and says that this Operator exists only in the semantics. I can not catch this idea ?.Furthermore, it gives a (syntactical- TLA+ level) definition as follows:

            ToBoolean(x) == x <--> TRUE    " x is Equivalent to TRUE "
the question here is , how can we compute the value of ToBoolean(5) and ToBoolean(ToBoolean(5)) with x not in the set BOOLEAN.

Thanks For Help.