chore: remove redundant words in comment

Signed-off-by: cuibuwei <[email protected]>

doc/papers/system-f-in-agda/paper.lagda

@@ -2618,7 +2618,7 @@ with conversion presented in section \ref{sec:intrinsically-typed}.
 We define two special cases of \AgdaFunction{subst} which allow us to
 substitute the types of variables or terms by propositionally equal
 types. While it is the case that types are now represented uniquely we
-still want or need to to prove that two types are equal, especially in
+still want or need to prove that two types are equal, especially in
 the presence of (Agda) variables, cf., while the natural number 7 has
 a unique representation in Agda we still might want to prove that for
 any natural numbers \AgdaBound{m} and \AgdaBound{n}, \AgdaBound{m}

doc/plutus-core-spec/flat-serialisation.tex

@@ -85,7 +85,7 @@ \subsection{Padding}
 then $\pad$ still adds an extra byte of padding; $\pad$ is used both for
 internal alignment (for example, to make sure that the contents of a bytestring
 are aligned on byte boundaries) and at the end of a complete encoding of a
-Plutus Core program to to make the length a multiple of 8 bits.
+Plutus Core program to make the length a multiple of 8 bits.
 Symbolically,
 $$
 \pad(s)  = s \cdot \pp{k} \quad \text{if $\length(s) = 8n+k$ with $n,k \in \N$ and $0 \leq k \leq 7$}