IndProp: fix minor formatting issues

Author: yurrriq

src/IndProp.lidr

@@ -104,18 +104,18 @@ When checking argument n to IndType.Wrong_ev:
                 Nat (Expected type)
 ```
 
-\todo[inline]{Edit the explanation, it works fine if you remove the first `n ->`
-in `Wrong_ev_SS`}
+\todo[inline]{Edit the explanation, it works fine if you remove the first \idr{n ->}
+in \idr{Wrong_ev_SS}}
 
 ("Parameter" here is Idris jargon for an argument on the left of the colon in an
 Inductive definition; "index" is used to refer to arguments on the right of the
 colon.)
 
-We can think of the definition of \idr{Ev} as defining a Idris property \idr{Ev
-: Nat -> Type}, together with theorems \idr{Ev_0 : Ev Z} and \idr{Ev_SS : n ->
-Ev n -> Ev (S (S n))}. Such "constructor theorems" have the same status as
-proven theorems. In particular, we can apply rule names as functions to each
-other to prove \idr{Ev} for particular numbers...
+We can think of the definition of \idr{Ev} as defining a Idris property
+\idr{Ev : Nat -> Type}, together with theorems \idr{Ev_0 : Ev Z} and
+\idr{Ev_SS : n -> Ev n -> Ev (S (S n))}. Such "constructor theorems" have the
+same status as proven theorems. In particular, we can apply rule names as
+functions to each other to prove \idr{Ev} for particular numbers...
 
 > ev_4 : Ev 4
 > ev_4 = Ev_SS {n=2} $ Ev_SS {n=0} Ev_0
@@ -1013,7 +1013,7 @@ We can solve this problem by generalizing over the problematic expressions with
 an explicit equality:
 
 ```coq
-Lemma star_app: ∀T (s1 s2 : list T) (re re' : Reg_exp T),
+Lemma star_app: forall T (s1 s2 : list T) (re re' : Reg_exp T),
   s1 =~ re' ->
   re' = Star re ->
   s2 =~ Star re ->
@@ -1035,7 +1035,7 @@ context. Here's how we can use it to show the above result:
 ```coq
 Abort.
 
-Lemma star_app: ∀T (s1 s2 : list T) (re : Reg_exp T),
+Lemma star_app: forall T (s1 s2 : list T) (re : Reg_exp T),
   s1 =~ Star re ->
   s2 =~ Star re ->
   s1 ++ s2 =~ Star re.
@@ -1075,7 +1075,7 @@ Star re', which results from the equality generated by remember.
 
   - (* MStarApp *)
     inversion Heqre'. rewrite H0 in IH2, Hmatch1.
-    intros s2 H1. rewrite ← app_assoc.
+    intros s2 H1. rewrite <- app_assoc.
     apply MStarApp.
     + apply Hmatch1.
     + apply IH2.
@@ -1266,8 +1266,8 @@ the second).
 > beq_natP : Reflect (n = m) (beq_nat n m)
 > beq_natP {n} {m} = iff_reflect $ iff_sym $ beq_nat_true_iff n m
 
-\todo[inline]{Edit -  we basically trade the invocation of `beq_nat_true` in
-`Left` for an indirect rewrite in `Right`}
+\todo[inline]{Edit - we basically trade the invocation of \idr{beq_nat_true} in
+\idr{Left} for an indirect rewrite in \idr{Right}}
 
 The new proof of \idr{filter_not_empty_In} now goes as follows. Notice how the
 calls to destruct and apply are combined into a single call to destruct.