proposition: Lemma extends_push : forall E x v, x # E -> extends E (E & x ~ v).
proof: Proof. Proof using. introv Fr. intros x' v' B. unfolds binds. rewrite get_push. case_if~. lets: get_none Fr. false. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)