elab-arr :
  % If
      {Elab : elab E (arr A B) (lamtm ([y] Mbody y))}
  % then
       step* E (lam ([x] Ebody x))
    -> ({x : exp} {y : tm} elab x A y -> elab (Ebody x) B (Mbody y))
  -> type.
%mode elab-arr +Elab -Steps -Elab'.


elab-arr/lam :     elab-arr (elab/arrintro Elab0) (step*/zero) Elab0.

elab-arr/merge1 :  elab-arr (elab/merge1 Elab1) (step*/left (step/unmerge left) Steps) ElabOut
                <- elab-arr Elab1 Steps ElabOut.

elab-arr/merge2 :  elab-arr (elab/merge2 Elab2) (step*/left (step/unmerge right) Steps) ElabOut
                <- elab-arr Elab2 Steps ElabOut.


%worlds ()     (elab-arr  _     _ _).
%total  (Elab) (elab-arr  Elab  _ _).