diff --git a/semester4/fmfp/parts/06_exercises/02_fm/02_axiomatic-semantics.tex b/semester4/fmfp/parts/06_exercises/02_fm/02_axiomatic-semantics.tex
index 01f5627..2b9292a 100644
--- a/semester4/fmfp/parts/06_exercises/02_fm/02_axiomatic-semantics.tex
+++ b/semester4/fmfp/parts/06_exercises/02_fm/02_axiomatic-semantics.tex
@@ -17,6 +17,8 @@ Of course, if \texttt{x} is decreasing, it itself can become the variant, as it
 Proof outlines work by providing post and pre-condition for each sub-statement in a statement.
 If we need to rewrite a statement (e.g. before the first loop body to change to our loop invariant from the overall precondition),
 we use the $\models$ symbol.
+Note that we want to describe each variable and for future assignments, we want to substitute all values with that assignments written out before
+they actually happen, for instance if down the line, in the same scope, we have \texttt{n := n - 1}, we substitute all occurrences of $n$ with $n - 1$ and update things accordingly.
 
 There are also tasks in which we need to find errors in rule applications. This works ``simply'' by checking that the rules are applied correctly
 and semantic entailment and general transformation rules hold for the transformations.
diff --git a/semester4/fmfp/parts/06_exercises/02_fm/04_ltl.tex b/semester4/fmfp/parts/06_exercises/02_fm/04_ltl.tex
index 6327f39..58199b8 100644
--- a/semester4/fmfp/parts/06_exercises/02_fm/04_ltl.tex
+++ b/semester4/fmfp/parts/06_exercises/02_fm/04_ltl.tex
@@ -43,3 +43,6 @@ These two properties are \textit{mutually exclusive} (with one exception, \textt
 In fact, every LTL formula is a either one of the two, or a conjunct of both.
 
 Finally, as a reminder, an LTL formula is for example $\square \Diamond A$, with $A$ an atomic proposition.
+
+Having an eventually in the formula fairly early on \textit{can} be an indicator that it is a liveness property,
+an always in the same positions \textit{can} indicate a safety property.