Kai

Lifting the binding prevents the error: ``` | L_p_4 -> let hErp_r = array_bget ( r.x, (0 : U32) ) !r in ( w , #{ hErp_pv_0 , r =...

It keeps shrinking. ``` type A f : (A!) -> Bool type R = #{ x : A, b : Bool } g : R -> R g r =...

Has anyone found a solution to this problem? I experience exactly the same, the buffer `*pvs*` shows ``` Starting pvs-sbclisp --noinform --no-userinit ... environment variable TMPDIR is not a writable...

I'm not entirely sure this is super-useful, but anyway, we can do a tiny bit better ``` powerset_finite3: JUDGEMENT powerset(B) HAS_TYPE non_empty_finite_set[finite_set[T]] ``` The proof (after having the previous one)...

This might be a smaller issue. Some files in lib/finite_sets appeared to have unfinished/untried proofs. I reran those and the .sequents files began to appear.

Accidentally closed. Sorry for the noise. I do believe it's still an issue.