Unsoundness due to bad simplification

[mtzguido]

(* culprit *)
let bad ()
  : Lemma (forall (f : int -> Type0). (forall (x : nat). f x) ==> f (-1)) = ()

let forall_elim (#a: Type) (p: (a -> GTot Type)) (x:a)
  : Lemma (requires forall (x: a). p x) (ensures p x) = ()

let falso () : Lemma False =
  bad();
  let f (x:int) : Type0 = x >= 0 in
  forall_elim #(int -> Type0) (fun f -> (forall (x : nat). f x) ==> f (-1)) f;
  ()

Posting a PR soon. The bad lemma is working due to a bad simplification step in the normalizer, which considers that f is universally true, so it's ok to rewrite f (-1) to True, failing of course to consider that nat is not int.