[Attempted to use "the method" also for big⇒small⇑.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080717234942
 + However, lack of inlining before productivity checking made this
   less appealing than for bar-thm and complete⇑.
] hunk ./Semantics/Equivalence.agda 133
+
+-- An alternative solution to the productivity problem. Unfortunately
+-- Agda does not normalise the right-hand sides (with the thing
+-- defined kept neutral) before checking productivity, so the code is
+-- not accepted. (And inlining lift⟶∞′ leads to less readable code,
+-- especially since it appears that some hidden arguments need to be
+-- given in order to keep the type checker happy.)
+
+-- lift⟶∞′ : forall {t i j x}
+--           (E : EvalCtxt t i j) ->
+--           Infinite″ (Step i) x ->
+--           Infinite″ (Step j) (E [ x ])
+-- lift⟶∞′ E = map∞′ (\x -> E [ x ]) (lift⟶ E)
+
+-- big⇒small⇑' : forall {t i} {e : Expr t} ->
+--               e ⇑[ i ] -> Infinite″ (Step i) (e ˢ)
+-- big⇒small⇑' (Loop ⇑)       ~ ↓ Red Loop ◅∞ big⇒small⇑' ⇑
+-- big⇒small⇑' (Add₁ x⇑)      ~ lift⟶∞′ (• •⊕ _) (big⇒small⇑' x⇑)
+-- big⇒small⇑' (Add₂ x↡ y⇑)   ~ lift⟶⋆ (• •⊕ _) (big⇒small⇓ (proj₂ x↡))
+--                                ◅◅∞′
+--                              lift⟶∞′ (nat proj₁ x↡ ⊕• •) (big⇒small⇑' y⇑)
+-- big⇒small⇑' (Seqn₁ x⇑)     ~ lift⟶∞′ (• •>> _) (big⇒small⇑' x⇑)
+-- big⇒small⇑' (Seqn₂ x↡ y⇑)  ~ lift⟶⋆ (• •>> _) (big⇒small⇓ (proj₂ x↡))
+--                                ◅◅∞′
+--                              (↓ Red Seqn₁ ◅∞ big⇒small⇑' y⇑)
+-- big⇒small⇑' (Catch₁ x⇑)    ~ lift⟶∞′ (• •catch _) (big⇒small⇑' x⇑)
+-- big⇒small⇑' (Catch₂ x↯ y⇑) ~ lift⟶⋆ (• •catch _) (big⇒small⇓ x↯)
+--                                ◅◅∞′
+--                              lift⟶∞′ (handler• •) (big⇒small⇑' y⇑)
+-- big⇒small⇑' (Block x⇑)     ~ lift⟶∞′ (block• •) (big⇒small⇑' x⇑)
+-- big⇒small⇑' (Unblock x⇑)   ~ lift⟶∞′ (unblock• •) (big⇒small⇑' x⇑)
+
+-- big⇒small⇑₂ : forall {t i} {e : Expr t} -> e ⇑[ i ] -> e ˢ ⟶∞[ i ]
+-- big⇒small⇑₂ ⇑ = ∞″→∞ (big⇒small⇑' ⇑)