Executable Specification

[View str.sig] [View str.mod]
sig str.

type   p, q, r          o.
module str.

r :- (p => q) => r.


[View str.thm]

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).
% p is independent of r.
Theorem indep : forall L,
  ctx L -> {L, p |- r} -> {L |- r}.