proposition: Lemma thinner_intersect_env_false1 : forall e e' b e1 e1', thinner_env e e' -> intersect_env false e b = Some e1 -> intersect_env false e' b = Some e1' -> thinner_env e1 e1'.
proof: Proof. intros e e' b e1 e1' Ht Hi1. destruct (intersect_env_false_accept e e' Ht b e1 Hi1) as [x [Hx Htx]]. rewrite Hx; intros He1'; injection He1'; intros; subst x; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom