proposition: Lemma thinner_widen : forall l l', thinner_env l (widen l l').
proof: Proof. induction l; intros l'. simpl; constructor. destruct a as [s v]; simpl. constructor; auto. apply Ab.thinner_widen. Qed.
imports: syntax little denot Bool List String ZArith axiom