proposition: Lemma join_widen2 : forall e e', compatible e e' -> (widen2 e) @@ e' = widen2 e.
proof: Proof. induction 1; try (simpl; auto; fail). unfold widen2, join_env; fold widen2; fold join_env; rewrite IHcompatible. rewrite Ab.join_comm; rewrite Ab.join_bot; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom