add two possible theorems to prove. run into issues with simplifying [if] expressions and [add]