Added some case (WLImp.v) of what I think he will ask us to prove once we prove our
Inductive theorems, tried to prove for While but always arrived to c =
WHILE BTrue DO c... not sure how to go around that one.