proposition: Lemma ok_concat_inv : forall E F, ok (E & F) -> ok E /\ ok F.
proof: Proof. Proof using. induction F using env_ind; rew_env_concat; introv Ok. auto. destruct (ok_push_inv Ok). destruct~ IHF. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)