proposition: Lemma thinner_eval : forall l l' a, thinner_env l l' -> Ab.thinner (ab_eval (ab_lookup l) a)(ab_eval (ab_lookup l') a).
proof: Proof. intros l l' a Hth; induction a; auto. simpl; apply thinner_lookup; auto. simpl; apply Ab.thinner_refl. simpl; apply Ab.thinner_plus; assumption. Qed.
imports: syntax little denot Bool List String ZArith axiom