| 23 | (Ignoring the coercions for the moment.) |

| 24 | |

| 25 | {{{ |

| 26 | norm [[F s1..sn ~ t]] = [[F s1'..sn' ~ t']] : eqs1++..++eqsn++eqt |

| 27 | where |

| 28 | (s1', eqs1) = flatten s1 |

| 29 | .. |

| 30 | (sn', eqsn) = flatten sn |

| 31 | (t', eqt) = flatten t |

| 32 | norm [[t ~ F s1..sn]] = norm [[F s1..sn ~ t]] |

| 33 | norm [[s ~ t]] = check [[s' ~ t']] : eqs++eqt |

| 34 | where |

| 35 | (s', eqs) = flatten s |

| 36 | (t', eqt) = flatten t |

| 37 | |

| 38 | check [[t ~ t]] = [] |

| 39 | check [[x ~ t]] | x `occursIn` t = fail |

| 40 | | otherwise = [[x ~ t]] |

| 41 | check [[t ~ x]] | x `occursIn` t = fail |

| 42 | | otherwise = [[x ~ t]] |

| 43 | check [[a ~ t]] | a `occursIn` t = fail |

| 44 | | otherwise = [[a ~ t]] |

| 45 | check [[t ~ a]] | a `occursIn` t = fail |

| 46 | | otherwise = [[a ~ t]] |

| 47 | check [[s1 s2 ~ t1 t2]] = check [[s1 ~ t1]] ++ check [[s2 ~ t2]] |

| 48 | check [[T ~ S]] = fail |

| 49 | |

| 50 | flatten [[F t1..tn]] = (x, [[F t1'..tn' ~ x]] : eqt1++..++eqtn) |

| 51 | where |

| 52 | (t1', eqt1) = flatten t1 |

| 53 | .. |

| 54 | (tn', eqtn) = flatten tn |

| 55 | NEW x |

| 56 | -- also need to add x := F t1'..tn' |

| 57 | flatten [[t1 t2]] = (t1' t2', eqs++eqt) |

| 58 | where |

| 59 | (t1', eqs) = flatten t1 |

| 60 | (t2', eqt) = flatten t2 |

| 61 | flatten t = (t, []) |

| 62 | }}} |

| 63 | |

| 64 | Notes: |