Some bug fixes while working on JFR version

src/Equality.v

@@ -574,7 +574,7 @@ Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == refl_equal x :=
 
 (** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial.
 
-   Suppose that we want to use [UIP_refl'] to establish another lemma of the kind of we have run into several times so far. *)
+   Suppose that we want to use [UIP_refl'] to establish another lemma of the kind we have run into several times so far. *)
 
 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
   O = match pf with refl_equal => O end.

src/Subset.v

@@ -71,7 +71,7 @@ Definition pred_strong1 (n : nat) : n > 0 -> nat :=
 
 (** We expand the type of [pred] to include a %\textit{%#<i>#proof#</i>#%}% that its argument [n] is greater than 0.  When [n] is 0, we use the proof to derive a contradiction, which we can use to build a value of any type via a vacuous pattern match.  When [n] is a successor, we have no need for the proof and just return the answer.  The proof argument can be said to have a %\textit{%#<i>#dependent#</i>#%}% type, because its type depends on the %\textit{%#<i>#value#</i>#%}% of the argument [n].
 
-One aspects in particular of the definition of [pred_strong1] that may be surprising.  We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions.  Let us see what happens if we write this function in the way that at first seems most natural.
+One aspect in particular of the definition of [pred_strong1] may be surprising.  We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions.  Let us see what happens if we write this function in the way that at first seems most natural.
 
 [[
 Definition pred_strong1' (n : nat) (pf : n > 0) : nat :=