1658   which we show again only for the Core Haskell example:

  1658   which we show again only for the interesting constructors in the Core Haskell

  1659 

  1659   example. We first show the weak induction principle for comparison:

  1660   

  1660 

  1661 \begin{equation}\nonumber

  1662 \infer

  1663 {

  1664   @{text "P1 tkind \<and> P2 ckind \<and> \<dots> \<and> P12 cvars"}

  1665 }{

  1666   \begin{tabular}{cp{7cm}}

  1667   @{text "P1 KStar"}\\

  1668   @{text "\<And>tk1 tk2. \<lbrakk>P1 tk1; P1 tk2\<rbrakk> \<Longrightarrow> P1 (KFun tk1 tk2)"}\\

  1669   @{text "\<dots>"}\\

  1670   @{text "\<And>v ty t1 t2. \<lbrakk>P3 ty; P7 t1; P7 t2\<rbrakk> \<Longrightarrow> P7 (Let v ty t1 t2)"}\\

  1671   @{text "\<And>p t al. \<lbrakk>P9 p; P7 t; P8 al\<rbrakk> \<Longrightarrow> P8 (ACons p t al)"}\\

  1672   @{text "\<dots>"}

  1673   \end{tabular}

  1674 }

  1675 \end{equation}

  1676 

  1677 

  1678 In comparison, the cases for the same constructors in the derived strong

  1679 induction principle are:

  1680 

  1681 \begin{equation}\nonumber

  1682 \infer

  1683 {

  1684   @{text "P1 a tkind \<and> P2 a ckind \<and> \<dots> \<and> P12 a cvars"}

  1685 }{

  1686   \begin{tabular}{cp{7cm}}

  1687   @{text "\<And>b. P1 b KStar"}\\

  1688   @{text "\<And>tk1 tk2 b. \<lbrakk>\<And>c. P1 c tk1; \<And>c. P1 c tk2\<rbrakk> \<Longrightarrow> P1 b (KFun tk1 tk2)"}\\

  1689   @{text "\<dots>"}\\

  1690   @{text "\<And>v ty t1 t2 b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c t1; \<And>c. P7 c t2; atom var \<sharp> b\<rbrakk> \<Longrightarrow> P7 b (Let v ty t1 t2)"}\\

  1691   @{text "\<And>p t al b. \<lbrakk>\<And>c. P9 c p; \<And>c. P7 c t; \<And>c. P8 c al; set (bv p) \<sharp>* b\<rbrakk> \<Longrightarrow> P8 b (ACons p t al)"}\\

  1692   @{text "\<dots>"}

  1693   \end{tabular}

  1694 }

  1695 \end{equation}

  1696