derivation-calculus-non-strictly-positive.v

derivation-calculus-non-strictly-positive.v

Inductive pl : Prop := disj: pl -> pl -> pl.

Definition context := pl -> Prop.

Reserved Notation "Gamma '|-' f" (at level 65).
Inductive plDerivable : context -> pl -> Prop :=

  disjElim: forall ctx (p q r: pl),
       ctx |- disj p q
    -> (ctx |- p -> ctx |- r)
    -> (ctx |- q -> ctx |- r)
    -> ctx |- r

  where "Gamma '|-' f" := (plDerivable Gamma f).
  
(* gives error:

  Non strictly positive occurrence of "plDerivable" in
    "forall (ctx : context) (p q r : pl),
    plDerivable ctx (disj p q) ->
    (plDerivable ctx p -> plDerivable ctx r) ->
    (plDerivable ctx q -> plDerivable ctx r) -> plDerivable ctx r".
  
*)