prove theorem about if statements!! using a clever destruct, overcome the previous nested induction one. also, understand how the bag theorem proof worked. 1. figure out more code to prove things about 2. figure out how coq works!