proposition: Lemma lt_interp_aux : forall f1 f2 i, (forall j, j <? i -> f1 j = f2 j) -> forall a, lt_atom i a -> interp_aux f1 a = interp_aux f2 a.
proof: Proof. intros f1 f2 i Hf; destruct a;simpl;intros;auto. rewrite Hf;trivial. unfold is_true in H;rewrite andb_true_iff in H;destruct H;rewrite !Hf;trivial. unfold is_true in H;rewrite !andb_true_iff in H;do 2 destruct H;rewrite !Hf;trivial. destruct n as [A]; replace (compute_interp f1 A nil l) with (compute_interp f2 A nil l); trivial; assert (H1: forall acc, compute_interp f2 A acc l = compute_interp f1 A acc l); auto; induction l as [ |k l IHl]; simpl; auto; intro acc; simpl in H; unfold is_true in H; rewrite andb_true_iff in H; destruct H as [H1 H2]; rewrite (Hf _ H1); destruct (f2 k) as [ta va]; destruct (Typ.cast ta A) as [ka| ]; auto. replace (List.map f1 l) with (List.map f2 l); trivial. induction l;simpl in H |- *;trivial. unfold is_true in H;rewrite andb_true_iff in H;destruct H;rewrite Hf, IHl;trivial. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList