proposition: Lemma lt_form_interp_form_aux : forall f1 f2 i h, (forall j, j <? i -> f1 j = f2 j) -> lt_form i h -> interp_aux f1 h = interp_aux f2 h.
proof: Proof. destruct h;simpl;intros;trivial; try (try apply afold_left_eq; try apply afold_right_eq;unfold is_true in H0; rewrite ?forallb_spec, ?aforallbi_spec, ?andb_true_iff in H0;intros; rewrite ?length_amap; try rewrite length_amap in H1; rewrite ?get_amap by assumption; auto using Lit.interp_eq_compat with smtcoq_core). - f_equal;auto using Lit.interp_eq_compat. - decompose [and] H0; rewrite !(Lit.interp_eq_compat f1 f2);auto. - decompose [and] H0; rewrite !(Lit.interp_eq_compat f1 f2);auto. - decompose [and] H0; rewrite !(Lit.interp_eq_compat f1 f2);auto. - replace (List.map (Lit.interp f2) l) with (List.map (Lit.interp f1) l); auto. unfold is_true in H0. rewrite List.forallb_forall in H0. apply List.map_ext_in. intros x Hx. apply Lit.interp_eq_compat; auto with smtcoq_core. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList