proposition: Lemma length_t_interp : length t_interp = length t_form.
proof: Proof. unfold t_interp. assert (Bt := to_Z_bounded (length t_form)). apply (foldi_ind _ (fun i a => length a = length t_form)). rewrite leb_spec, to_Z_0; lia. rewrite length_make, leb_length; reflexivity. intros;rewrite length_set;trivial. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList