proposition: Lemma compatible_update : forall l s e, compatible l (ab_update l s e).
proof: Proof. induction l; simpl. intros s e; apply cc1. destruct a as [s0 i0]; intros s e; destruct (string_dec s s0); constructor; auto. apply compatible_refl. Qed.
imports: syntax little denot Bool List String ZArith axiom