proposition: Lemma join_env_assoc : forall l l' l'', (l @@ l') @@ l'' = l @@ l' @@ l''.
proof: Proof. induction l; destruct l'; destruct l''; simpl; auto. destruct p; auto. destruct p; destruct p0; try destruct a; auto. destruct a; auto. destruct a; auto. destruct a; auto. destruct p; auto. destruct a; auto. destruct p; auto. destruct p0; auto. simpl; rewrite join_assoc; rewrite IHl; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom