proposition: Lemma binds_weaken : forall x a E F G, binds x a (E & G) -> ok (E & F & G) -> binds x a (E & F & G).
proof: Proof. Proof using. introv H O. lets [?|[? ?]]: binds_concat_inv H. applys~ binds_concat_right. applys~ binds_concat_left. applys~ binds_concat_left_ok. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)