-subterms, and to use coerce recursively on the subterms using the
-generated equalities. This interplay between the canonicity of equated
-types, type equalities, and \myfun{coe} ensures that invocations of
-$\myfun{coe}$ will vanish when we have evidence of the structural
-equality of the types we are transporting terms across. If the type is
-neutral, the equality will not reduce and thus $\myfun{coe}$ will not
-reduce either. If we come across an equality between different
-canonical types, then we reduce the equality to bottom, making sure that
-no such proof can exist, and providing an `escape hatch' in
-$\myfun{coe}$.
+subterms. So if are equating two product types, the equality will
+reduce to two subequalities regarding the first and second type. Then,
+we can \myfun{coe}rce to transport values between equal types.
+Following the subequalities, \myfun{coe} will procede recursively on the
+subterms.
+
+This interplay between the canonicity of equated types, type
+equalities, and \myfun{coe}, ensures that invocations of $\myfun{coe}$
+will vanish when we have evidence of the structural equality of the
+types we are transporting terms across. If the type is neutral, the
+equality will not reduce and thus $\myfun{coe}$ will not reduce either.
+If we come across an equality between different canonical types, then we
+reduce the equality to bottom, making sure that no such proof can exist,
+and providing an `escape hatch' in $\myfun{coe}$.