proposition: Lemma interp_check_form_aux : forall a b, check_form_aux a b -> Form.interp interp_form_hatom interp_form_hatom_bv t_form a = Form.interp interp_form_hatom interp_form_hatom_bv t_form b.
proof: Proof. intros [a| | |i1 l1|a1|a1|a1|l1 l2|l1 l2|l1 l2 l3|a l1] [b| | |j1 m1|a2|a2|a2|j1 j2|j1 j2|j1 j2 j3|b m1]; simpl; try discriminate;auto with smtcoq_core. unfold is_true; rewrite Int63.eqb_spec; intro; subst a; auto with smtcoq_core. apply interp_check_distinct; auto with smtcoq_core. unfold is_true; rewrite andb_true_iff, Int63.eqb_spec; intros [H1 H2]; subst j1. rewrite (interp_check_lit _ _ H2). auto with smtcoq_core. unfold is_true; rewrite andb_true_iff, eqb_spec, aforallbi_spec; intros [H1 H2]; apply afold_left_eq; rewrite ?length_amap; auto with smtcoq_core; intros i Hi; rewrite 2!get_amap by (rewrite <- ?H1; assumption); apply interp_check_lit; auto with smtcoq_core. unfold is_true; rewrite andb_true_iff, eqb_spec, aforallbi_spec; intros [H1 H2]; apply afold_left_eq; rewrite ?length_amap; auto with smtcoq_core; intros i Hi; rewrite 2!get_amap by (rewrite <- ?H1; assumption); apply interp_check_lit; auto with smtcoq_core. unfold is_true; rewrite andb_true_iff, eqb_spec, aforallbi_spec; intros [H1 H2]; apply afold_right_eq; rewrite ?length_amap; auto with smtcoq_core; intros i Hi; rewrite 2!get_amap by (rewrite <- ?H1; assumption); apply interp_check_lit; auto with smtcoq_core. unfold is_true; rewrite andb_true_iff; intros [H1 H2]; rewrite (interp_check_lit _ _ H1), (interp_check_lit _ _ H2); auto with smtcoq_core. unfold is_true; rewrite andb_true_iff; intros [H1 H2]; rewrite (interp_check_lit _ _ H1), (interp_check_lit _ _ H2); auto with smtcoq_core. unfold is_true; rewrite !andb_true_iff; intros [[H1 H2] H3]; rewrite (interp_check_lit _ _ H1), (interp_check_lit _ _ H2), (interp_check_lit _ _ H3); auto with smtcoq_core. Qed.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms