Fixing crash in proof obligation expression computation

[marcoeilers]

This code could crash because the list of subconditions for And, Or and Implies actually returns three lists of subnodes instead of two, which the code expected. This is because it return one list per subnode, and the subnodes include the type of the node, which is why there are three subnodes for binary operations.