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