refl --> eq.refl

04_Quantifiers_and_Equality.org

@@ -355,7 +355,7 @@ calc
 Each =<proof>_i= is a proof for =<expr>_{i-1} op_i <expr>_i=. The
 =<proof>_i= may also be of the form ={ <pr> }=, where =<pr>= is a
 proof for some equality =a = b=. The form ={ <pr> }= is just syntactic
-sugar for =eq.subst <pr> (refl <expr>_{i-1})= In other words, we are
+sugar for =eq.subst <pr> (eq.refl <expr>_{i-1})= In other words, we are
 claiming we can obtain =<expr>_i= by replacing =a= with =b= in
 =<expr>_{i-1}=.