proposition: Lemma thinner_update : forall l l' s i1 i2, thinner_env l l' -> Ab.thinner i1 i2 -> thinner_env (ab_update l s i1) (ab_update l' s i2).
proof: Proof. intros l l' s i1 i2 Hte Hth; induction Hte. simpl; apply cte1. simpl. destruct (string_dec s s0);apply cte2; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom