proposition: Lemma join_env_comm : forall l l', compatible l l' -> l @@ l' = l' @@ l.
proof: Proof. induction 1; auto. simpl; rewrite join_comm; rewrite IHcompatible; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom