Specification "str". Define ctx : olist -> prop by ctx nil; ctx ((p => q) :: L) := ctx L. Theorem ctx_mem : forall L E, ctx L -> member E L -> E = (p => q). induction on 2. intros. case H2. case H1. search. case H1. apply IH to H4 H3. search. % p is independent of r. Theorem indep : forall L, ctx L -> {L, p |- r} -> {L |- r}. induction on 2. intros. case H2. apply IH to _ H3. search. case H4. case H3. apply ctx_mem to _ H5. case H3.