proposition: Lemma empty_concat_inv : forall E F, empty = E & F -> empty = E /\ empty = F.
proof: Proof. Proof using. introv H. rew_env_defs. forwards*: nil_eq_app_inv H. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)