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