Click on a command or tactic to see a detailed view of its use.

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.