proposition: Lemma thinner_join_env_right : forall e e', compatible e e' -> thinner_env e (e' @@ e).
proof: Proof. intros e e' H; induction H; simpl. apply cte1. apply cte2; auto. apply thinner_join_right. Qed.
imports: syntax little denot Bool List String ZArith axiom