added some comments

README

@@ -2,6 +2,12 @@ This project was built with coq version 8.7.2.
 
 This project uses Autosubst (https://github.com/uds-psl/autosubst). It must be installed from the coq86-devel branch as described in the README of Autosubst.
 
+For inversion the inverts ... as tactic from lib/LibTactics.v is used.
+
+Naming convention:
+GQM-Formulas: A,B,C..., sometimes f,g,...
+Context: c
+
 To build the project run
 $ make
 

theories/Section5.v

@@ -69,6 +69,7 @@ Lemma lemma_A_3 : forall A, (|-- [A]A <<->> [A]A).
 Proof.
   move => A.
   hSplit; first by apply: gqm_id.
+  (* this direction could also be proved by gqm_id, but we what to check, that the proof from the paper works as well *)
   (* (1) *)
   have H1 := (gqm_Aglob (A._[ren_ (0 .: (+2))]) (Var 0)).
   asimpl in H1.

theories/Section5WithContext.v

@@ -32,6 +32,7 @@ Proof.
   move => c A.
   split.
   - elim; clear c A => c A.
+    (* the inverts and inverts ... as tactics are from lib/LibTactics.v *)
     + elim: c A; first by move => ? Hi; inverts Hi.
       move => f l IH A Hi /=.
       inverts Hi as.