[Made it easier (?) to apply the right-assoc lemma.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080303000703
 + In the left-to-right direction.
] hunk ./MultiComposition.agda 58
+-- Note the similarity between merge and split...
+
hunk ./MultiComposition.agda 65
-_⟪_⟫'_ : forall {a b ts₂} ->
-         Fun (a ∷ ts₂) b -> (ts₁ : TypeList) ->
-         Fun ts₁ a -> Fun (ts₁ ++ ts₂) b
-f ⟪ ts₁ ⟫' g = merge ts₁ (f ⟪ ts₁ ⟫ g)
-
--- This function is more obviously related to _⟪_⟫_, but the use of
--- substitutivity makes it harder to prove things about it.
--- Furthermore _⟪_⟫'_ above has the same computational behaviour as
--- _⟪_⟫_.
---
--- _⟪_⟫'_ : forall {a b ts₂} ->
---          (a -> Fun ts₂ b) -> (ts₁ : TypeList) ->
---          Fun ts₁ a -> Fun (ts₁ ++ ts₂) b
--- f ⟪ ts₁ ⟫' g = ≡₁-subst (lemma ts₁) (f ⟪ ts₁ ⟫ g)
+split : forall {a} ts₁ {ts₂} ->
+        Fun (ts₁ ++ ts₂) a -> Fun ts₁ (Fun ts₂ a)
+split []        f = f
+split (t ∷ ts₁) f = \x -> split ts₁ (f x)
hunk ./MultiComposition.agda 70
-right-assoc : forall {a b t} ts₁ {ts₂}
+right-assoc : forall {a b t} ts₁ ts₂
hunk ./MultiComposition.agda 72
-              (f ⟪ t ∷ ts₂ ⟫ g) ⟪ ts₁ ⟫' h ≡
-              f ⟪ ts₁ ++ ts₂ ⟫ (g ⟪ ts₁ ⟫' h)
-right-assoc []         f g h = ≡-refl
-right-assoc (t₁ ∷ ts₁) f g h = ≡-ext \x -> right-assoc ts₁ f g (h x)
+              (f ⟪ t ∷ ts₂ ⟫ g) ⟪ ts₁ ⟫ h ≡
+              split ts₁ (f ⟪ ts₁ ++ ts₂ ⟫ (merge ts₁ (g ⟪ ts₁ ⟫ h)))
+right-assoc []         ts₂ f g h = ≡-refl
+right-assoc (t₁ ∷ ts₁) ts₂ f g h =
+  ≡-ext \x -> right-assoc ts₁ ts₂ f g (h x)