Reduce boilerplate to merge local predicates

[TWal]

Currently, some amount of boilerplate is needed to merge local predicates, and prove that the global predicate contains all local predicates:

dolev-yao-star-extrinsic/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst

Lines 110 to 123 in 297eeb7

	val all_sessions_has_all_sessions: unit -> Lemma (norm [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate protocol_invariants_nsl) all_sessions))
	let all_sessions_has_all_sessions () =
	assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_sessions)));
	mk_global_local_bytes_state_predicate_correct protocol_invariants_nsl all_sessions;
	norm_spec [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate protocol_invariants_nsl) all_sessions)
	val protocol_invariants_nsl_has_pki_invariant: squash (has_pki_invariant protocol_invariants_nsl)
	let protocol_invariants_nsl_has_pki_invariant = all_sessions_has_all_sessions ()
	val protocol_invariants_nsl_has_private_keys_invariant: squash (has_private_keys_invariant protocol_invariants_nsl)
	let protocol_invariants_nsl_has_private_keys_invariant = all_sessions_has_all_sessions ()
	val protocol_invariants_nsl_has_nsl_session_invariant: squash (has_local_state_predicate protocol_invariants_nsl state_predicate_nsl)
	let protocol_invariants_nsl_has_nsl_session_invariant = all_sessions_has_all_sessions ()

The boilerplate is linear in the number of local predicates, there is no reason that this shouldn't be doable in constant size? For example using a meta-program?