let stats_nb_proof_tree_nodes = ref 0