proposition: Lemma thinner_widen2 : forall l, thinner_env l (widen2 l).
proof: Proof. induction l. apply cte1. destruct a as [s p]; simpl; apply cte2. apply Ab.thinner_bot. auto. Qed.
imports: syntax little denot Bool List String ZArith axiom