sub-refl :
  % If
     {A : tp}
  % then
     {Coe : exp -> exp}
     {CoeTyping : {e:exp} typeof e A -> typeof (Coe e) A}
     sub A A Coe CoeTyping
 -> type.
%mode sub-refl +A
               -Coe -CoeTyping -Sub.

- :   sub-refl topty _ _ (sub/top-right).

- :   sub-refl (arr A1 A2) _ _ (sub/arr Sub1 Sub2)
   <- sub-refl A1 _ _ Sub1
   <- sub-refl A2 _ _ Sub2.

- :   sub-refl (sectty A1 A2) _ _ (sub/sect-right (sub/sect-left-1 Sub1) (sub/sect-left-2 Sub2))
   <- sub-refl A1 _ _ Sub1
   <- sub-refl A2 _ _ Sub2.

- :   sub-refl (unty A1 A2) _ _ (sub/union-left (sub/union-right-1 Sub1) (sub/union-right-2 Sub2))
   <- sub-refl A1 _ _ Sub1
   <- sub-refl A2 _ _ Sub2.


%worlds () (sub-refl  _  _ _ _).
%total  A  (sub-refl  A  _ _ _).