started deduction with contexts

_CoqProject

+-Q lib GQM.Lib
 -Q theories GQM
 -arg -w -arg -notation-overridden
 theories/Base.v
 theories/GQM.v
-theories/GQMDeduction.v
\ No newline at end of file
+theories/GQMDeduction.v
+lib/LibTactics.v
\ No newline at end of file

theories/Base.v

 From Coq Require Export ssreflect ssrfun ssrbool.
-Require Export Coq.Lists.List.
-Export ListNotations.
+Require Export Autosubst.Autosubst.
+Require Export Coq.Sets.Ensembles.
+Require Export GQM.Lib.LibTactics.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

theories/GQM.v

-Require Import Autosubst.Autosubst.
-
 Require Import GQM.Base.
 
 Inductive form :=
 | Var (x : var)
-| Neg (f : form)
-| And (f g : form)
+| Imp (f g : form)
 | Box (f : form)
 | SquareAll (f : {bind form}).
 
@@ -14,18 +11,18 @@ Instance Rename_form : Rename form. derive. Defined.
 Instance Subst_form : Subst form. derive. Defined.
 Instance SubstLemmas_form : SubstLemmas form. derive. Qed.
 
-Infix "&" :=  And (at level 75, right associativity).
 Notation "'[A]' B"   := (SquareAll B) (at level 74, right associativity).
 Notation "|[]| A"   := (Box A) (at level 74, right associativity).
+Notation "A '->>' B" := (Imp A B) (at level 77, right associativity).
+Definition Bot := [A] (Var 0).
+Definition Neg A := A ->> Bot.
 Notation "'-!' A" := (Neg A) (at level 73, right associativity).
-Definition Or A B := (-! (-! A & -! B)).
+Definition Or A B := (-! A ->> B).
 Notation "A '|||' B" := (Or A B) (at level 76, right associativity).
-Definition Imp A B := ((-! A) ||| B).
-Notation "A '->>' B" := (Imp A B) (at level 77, right associativity).
+Definition And A B := -! ( A ->> -! B).
+Infix "&" :=  And (at level 75, right associativity).
 Notation "A '<<->>' B" := ((A ->> B) & (B ->> A)) (at level 78).
 
-Notation context := (list form).
-
 (** ** Decidable Equality *)
 
 Lemma dceq_v : forall n n0,  {Var n = Var n0} + {Var n <> Var n0}.