mushrm88

I can use `tcnorm` to fix this particular example, but that causes a bunch of problems elsewhere: ```fstar [@@tcnorm] type elem (index : nat) = main index ``` I can...

@aseemr This was a big help and I was able to remove many ascriptions and all `assume`s from my code. Thanks! I don't really understand why hoisting the refinement makes...