proposition: Lemma extends_concat_r : forall E F, disjoint (dom E) (dom F) -> extends E (E & F).
proof: Proof. Proof using. introv D B. unfolds binds. lets: get_some_inv A B. forwards M: get_none A x F. applys~ disjoint_in_notin D. rewrite get_concat. rewrite~ M. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)