Add wp_if_join tactic

[codyjrivera]

I add a tactic, wp_if_join, that allows you to 'join' both branches of an if-statement into a single assertion by showing that both branches make said assertion hold.

Given the program below (and assertion A)

if b { S1; } else { S2; } // no `else` is handled trivially by Goose.
// assertion `A`
S3;

By using the tactic wp_if_join <assertion> [with <ipat>] (leaving off the with to provide no spatial hypotheses), the goal is split into three subgoals:

1. Proving that S1 results in A holding,
2. Proving that S2 results in A holding, and
3. Proving the remainder of the program, S3, assuming that A holds.