Binding environment in Lemmas

[briangmilnes]

I have to do things like:
let flatten_seq_elt'_step
(#a: eqtype)
(s: seq'nz (seq' a))
(index_seq: seq'nz nat{flatten_index_seq s index_seq})
(s': seq' a{length' s' = flat_length' s})
(seg : nat{seg < length' s})
(elt : nat{elt < length' (nth' s seg) /\ flattened_upto_seg_elt #a s index_seq s' seg elt})
: Lemma (ensures flat_length_upto'_seg_off_lt_flat_length' s seg elt; // An application of a lemma in a lemma.
let s'' = update' s' ((nth' index_seq seg) + elt) (nth' (nth' s seg) elt) in
flattened_upto_seg_elt s index_seq s'' seg (elt + 1))
= flat_length_upto'_seg_off_lt_flat_length' s seg elt; // An application of a lemma in a lemma.
let s'' = update' s' ((nth' index_seq seg) + elt) (nth' (nth' s seg) elt) in
...
on occasion.

A wish list level item might be to allow a different binding environment. I could make s'' an argument but the lemma
requirement has to stay.