proposition: Lemma valid_C_true : C.interp rho C._true.
proof: Proof. apply C.interp_true. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form);trivial. Qed.
imports: Bool List Int63 PArray State SMT_terms