60 | | v ~ [x], F v ~ x |

| 61 | [F v] ~ v ||- [F v] ~ v |

| 62 | ==> normalise |

| 63 | v ~ [a], F v ~ a ||- v ~ [x], F v ~ x |

| 64 | a := F v |

| 65 | ==> (IdenticalLHS) with v & F v |

| 66 | v ~ [a], F v ~ a ||- [a] ~ [x], x ~ a |

| 67 | ==> normalise |

| 68 | v ~ [a], F v ~ a ||- x ~ a, x ~ a |

| 69 | ==> (Unify) |

| 70 | v ~ [a], F v ~ a ||- a ~ a |

| 71 | ==> normalise |

| 72 | v ~ [a], F v ~ a ||- |

| 73 | QED |

| 74 | }}} |

| 75 | |

| 76 | Derivation our modified rules: |

| 77 | {{{ |

| 78 | [F v] ~ v ||- [F v] ~ v |

| 79 | ==> normalise |

| 80 | v ~ [x2], F v ~ x2 ||- v ~ [x1], F v ~ x1 |

| 81 | ** x2 := F v |

62 | | v ~ [x], F [a] ~ x |

63 | | ==> (Top) |

64 | | v ~ [x], x ~ [F x] |

65 | | ===> normalise |

66 | | v ~ [x], x ~ [y], F x ~ y |

| 83 | F [x2] ~ x2 ||- [x2] ~ [x1], F [x2] ~ x1 |

| 84 | ** x2 := F v |

| 85 | ==> normalise |

| 86 | F [x2] ~ x2 ||- x2 ~ x1, F [x2] ~ x1 |

| 87 | ** x2 := F v |

| 88 | ==> 2x (Top) & Unify |

| 89 | [F x1] ~ x1 ||- [F x1] ~ x1 |

| 90 | ** x1 := F v |

| 91 | ==> normalise |

| 92 | x1 ~ [y2], F x1 ~ y2 ||- x1 ~ [y1], F x1 ~ y1 |

| 93 | ** x1 := F v, y2 := F x1 |

| 94 | ..we stop here if (Local) doesn't apply to flexible tyvars |