Tactics create unprovable guards

The code type checks fine without tactics, but fails when using tactics (both version 1 and 2). 

```fstar
assume val z : nat

let f () : Pure (nat -> nat) (z > 0) (fun _ -> True) by (  
   let p = forall_intro () in
   let h = implies_intro () in
   dump "H") =
  (fun x -> x / z)
```