Index: doc/theses/fangren_yu_MMath/intro.tex
===================================================================
--- doc/theses/fangren_yu_MMath/intro.tex	(revision 1e7e6f383fe5f9e7bbf40293a6b9a6f4d470de5b)
+++ doc/theses/fangren_yu_MMath/intro.tex	(revision 98c77b23c65a940cf9e4e2811e0737d6305418e2)
@@ -912,8 +912,10 @@
 For software-engineering reasons, the set assertions would be refactored into a trait to allow alternative implementations, like a Java \lstinline[language=java]{interface}.
 
-In summation, the \CFA type system inherits \newterm{nominal typing} for concrete types from C, and adds \newterm{structural typing} for polymorphic types.
-Traits are used like interfaces in Java or abstract base-classes in \CC, but without the nominal inheritance relationships.
-Instead, each polymorphic function or generic type defines the structural type needed for its execution, which is fulfilled at each call site from the lexical environment, like Go~\cite{Go} or Rust~\cite{Rust} interfaces.
-Hence, new lexical scopes and nested functions are used extensively to create local subtypes, as in the @qsort@ example, without having to manage a nominal inheritance hierarchy.
+In summation, the \CFA type system inherits \newterm{nominal typing} for concrete types from C;
+however, without inheritance in \CFA, nominal typing cannot be extended to polymorphic subtyping.
+Instead, \CFA adds \newterm{structural typing} and uses it to generate polymorphism.
+Here, traits are like interfaces in Java or abstract base-classes in \CC, but without the nominal inheritance relationships.
+Instead, each polymorphic function or generic type defines the structural requirements needed for its execution, which is fulfilled at each call site from the lexical environment, like Go~\cite{Go} or Rust~\cite{Rust} interfaces.
+Hence, lexical scopes and nested functions are used extensively to mimic subtypes, as in the @qsort@ example, without managing a nominal inheritance hierarchy.