By definition of Implication operator, false -> true and false -> false. It means that
false implies any predicate, no matter true or false. We don't need to go any further
trying to prove the statement we need and just always say that false implies it in this case.
In practice it means that we are trying to prove something guarded by false condition,
which means that this code is unreachable, and we can safely prove any fact or perform any
transform in this code.