proposition: Lemma thinner_join_env : forall e1 e2 e3 e4, compatible e1 e3 -> thinner_env e1 e2 -> thinner_env e3 e4 -> thinner_env (e1 @@ e3)(e2 @@ e4).
proof: Proof. intros e1 e2 e3 e4 Hc H; generalize e3 e4 Hc; clear e3 e4 Hc. induction H; simpl. intros e3 e4 Hc; inversion Hc; intros Ht3; inversion Ht3; apply cte1. intros e3 e4 Hc; inversion Hc; intros Ht3; inversion Ht3; apply cte2; auto. apply Ab.thinner_join; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom