elab-inl :
    % If
       {ElabIn : elab E (unty A1 A2) (inl M0)}
    % then
        elab E A1 M0
 -> type.
%mode elab-inl +ElabIn -ElabOut.

- :
       elab-inl (elab/unintro1 Elab0) Elab0.

- :
       elab-inl (elab/merge1 Elab1) (elab/merge1 Elab0)
    <- elab-inl Elab1 Elab0.

- :
       elab-inl (elab/merge2 Elab2) (elab/merge2 Elab0)
    <- elab-inl Elab2 Elab0.


%worlds ()     (elab-inl  _       _).
%total  ElabIn (elab-inl  ElabIn  _).



elab-inr :
    % If
       {ElabIn : elab E (unty A1 A2) (inr M0)}
    % then
        elab E A2 M0
 -> type.
%mode elab-inr +ElabIn -ElabOut.

- :
       elab-inr (elab/unintro2 Elab0) Elab0.

- :
       elab-inr (elab/merge1 Elab1) (elab/merge1 Elab0)
    <- elab-inr Elab1 Elab0.

- :
       elab-inr (elab/merge2 Elab2) (elab/merge2 Elab0)
    <- elab-inr Elab2 Elab0.


%worlds ()     (elab-inr  _       _).
%total  ElabIn (elab-inr  ElabIn  _).