rewrite components not checked?

[mtzguido]

This works, despite the ill-typed if.

```pulse
ghost
fn test (_:unit)
  requires emp
  ensures emp
{
  rewrite emp as (if true then emp else 1);
  admit();
}
```

[aseemr]

I was looking at it today. We do send a query to typecheck the argument, and core checker successfully typechecks the term at type vprop. My guess is because of iota reduction. If we write it as if false then emp else 1 then it fails.