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

Specification "str1".

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.
%% This lemma is NOT provable since r depends on q 
%% which in turn depends on p. 
Theorem indep : 
   (forall L,
      ctx L -> {L, p |- p} -> {L |- p})
/\ (forall L,
      ctx L -> {L, p |- q} -> {L |- q})
/\ (forall L,
      ctx L -> {L, p |- r} -> {L |- r}).
induction on 2 2 2. intros. split. 
  % p is independent of p (which is NOT provable)
  intros. case H2. 
    case H4. 
      case H3. skip. % Cannot proceed
      apply ctx_mem to _ H5. case H3.
  % p is independent of q (again, not provable)
  intros. case H2.
    case H4.
      case H3.
      apply ctx_mem to _ H5. case H3.
        % application of IH which is not provable
        apply IH to _ H6. search.
  % p is independent of r (not provable)
  intros. case H2.
    apply IH2 to _ H3. search.
    % application of IH1 which is not provable
    apply IH1 to _ H3. search.
    case H4.
      case H3.
      apply ctx_mem to _ H5. case H3.