(****************************************************************************)
(*                             predicates.v                                 *)
(*                                                                          *)
(*                             Pierre Lescanne                              *)
(*                                                                          *)
(*		       LIP (ENS-Lyon, CNRS, INRIA)                          *)
(*                                                                          *)
(*                                                                          *)
(* Developed in V7.4    March  2004                                         *)
(****************************************************************************)
Section Barcan.

Require axioms.
Require minimal.
Require propositional.
Require predicates.
Require or_and_exist.
Require modal.

Notation "|- p" := (theorem p) (at level 7).
Infix RIGHTA 5 "=>" Imp.

Notation "\-/ p" := (Forall ? p) (at level 5, right associativity).

Axiom Barcan : (A:Set)(i: nat)(P:A->proposition)
    |- (\-/[a:A](K i (P a)))  => (K i (\-/P)).

Theorem Barcan1 : (A:Set) (i: nat)(P:A->proposition)
    ((a:A) |- (K i (P a))) -> |- (K i (\-/P)).
Proof.
Intros.
Apply MP with (\-/[a:A](K i (P a))).
Apply Barcan.
Apply ForallRule.
Apply H.
Qed.

End Barcan.