1349   introduced the term has the support equal to @{text "{x}"}.

  1349   introduced the term has the support equal to @{text "{x}"}. 

  1350 

  1350 

  1351   We will now show that the quotient types have a finite support.

  1351   To show the support equations for the lifted types we want to use the

  1352 

  1352   Lemma \ref{suppabs}, so we start with showing that they have a finite

  1353 

  1353   support.

  1354 

  1354 

  1355 

  1355   \begin{lemma} The types @{text "ty\<^isup>\<alpha>\<^isub>1 \<dots> ty\<^isup>\<alpha>\<^isub>n"} have finite support.

  1356   \end{lemma}

  1357   \begin{proof}

  1358   By induction on the lifted types. For each constructor its support is

  1359   supported by the union of the supports of all arguments. By induction

  1360   hypothesis we know that each of the recursive arguments has finite

  1361   support. We also know that atoms and finite atom sets and lists that

  1362   occur in the constructors have finite support. A union of finite

  1363   sets is finite thus the support of the constructor is finite.

  1364   \end{proof}

  1365 

  1366   \begin{lemma} For each lifted type @{text "ty\<^isup>\<alpha>\<^isub>i"}, for every @{text "x"}

  1367    of this type:

  1368   \begin{center}

  1369   @{term "supp x = fv_ty\<^isup>\<alpha>\<^isub>i x"}.

  1370   \end{center}

  1371   \end{lemma}

  1372   \begin{proof}

  1373   By induction on the lifted types, together with the equations that characterize

  1374   @{term "fv_bn"} in terms of @{term "supp"}...

  1375   \end{proof}