Squash confusion in calc proofs

[mtzguido]

This works just fine, even if the lemma works on squashes (or on just pp/qq)

assume val pp : prop
assume val qq : prop
assume val ii : unit -> Lemma (requires squash pp) (ensures squash qq)

let test () =
  calc (==>) {
    pp;
    ==> { ii () }
    qq;
  }

This fails:

assume val pp : prop
assume val qq : prop
assume val ii : unit -> Lemma (requires squash pp) (ensures squash qq)

let test () =
  calc (==>) {
    squash pp;
    ==> { ii () }
    squash qq;
  }