in citp in fun select #CITP# . loop init . ---> Proof: *** 1 *** (goal FG-FUN |- eq 9 <= G(F(X:Nat))+ G(X:Nat)= true ;) *** 2 *** (tc ca red) ---> QED