proposition: Lemma compatible_thinner_widen2 : forall l l', compatible l l' -> thinner_env l (widen2 l').
proof: Proof. induction 1; simpl; try constructor; auto. apply Ab.thinner_bot. Qed.
imports: syntax little denot Bool List String ZArith axiom