proposition: Lemma thinner_lookup : forall l l' s, thinner_env l l' -> Ab.thinner (ab_lookup l s)(ab_lookup l' s).
proof: Proof. induction 1; unfold ab_lookup; simpl. apply Ab.thinner_refl. destruct (string_dec s0 s); auto. Qed.
imports: syntax little denot Bool List String ZArith axiom