proposition: Lemma default_t_form : default t_form = Ftrue.
proof: Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form) as [[H _] _]; auto. Qed.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms