proposition: Lemma get_none_inv : forall x E, get x E = None -> x # E.
proof: Proof. Proof using. induction E using env_ind; introv Eq. simpl_dom. auto. rewrite get_push in Eq. case_if~. simpl_dom. auto. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)