# [PVS-HELP] about Inst. existential quantifiers

Dear Everyone:

I have a sequent as follow, I want to inst the quantifier the deepest one as  (EXISTS (s: State[Vars]) in the example.

How can I do? Thanks

EXISTS (s_1: State[Vars]):
(EXISTS (s_8: State[Vars]):
(EXISTS (s_7: State[Vars]):
(EXISTS (s_6: State[Vars]):
(EXISTS (s_5: State[Vars]):
(EXISTS (s_4: State[Vars]):
(EXISTS (s_3: State[Vars]):
(EXISTS (s_2: State[Vars]):
(EXISTS (s: State[Vars]):
intro(x)(Init_state, s) AND
intro(y)(s, s_2))
AND intro(z)(s_2, s_3))
AND intro(max)(s_3, s_4))
AND intro(min)(s_4, s_5))
AND intro(aver)(s_5, s_6))
AND assign(x, 1)(s_6, s_7))
AND assign(y, 3)(s_7, s_8))
AND assign(z, 8)(s_8, s_1))
AND
(c(LAMBDA (s1_1, s2_1: State[Vars]):
EXISTS (s_1: State[Vars]):
assign(max, x)(s1_1, s_1) AND
(EXISTS (s: State[Vars]):
IFELSE((max > y), skip, assign(max, y))(s_1, s) AND
IFELSE((max > z), skip, assign(max, z))(s, s2_1)),
LAMBDA (s1_1, s2_1: State[Vars]):
EXISTS (s_1: State[Vars]):
assign(min, x)(s1_1, s_1) AND
(EXISTS (s: State[Vars]):
IFELSE((min < y), skip, assign(min, y))(s_1, s) AND
IFELSE((min < z), skip, assign(min, z))(s, s2_1)))
// assign(aver, exp(x, y, z)))
(s_1, s_end)