% "Summary" results, which just compose various theorems.

% summary-static:  If . |- e : A in the full (including subsumption) source typing system,
%                  then there exists e' such that . |- e' : A elaborates to M
%                                             and . |- M : A  in the target type system.

summary-static :
   % If
        typeof+sub E A
   % then
     -> elab E' A M
     -> typeoftm M A
  -> type.
%mode summary-static +DwithSubsumption
                     -Elab -Dtarget.

- :
     summary-static DwithSubsumption Elab Dtarget
  <- coerce E DwithSubsumption EwithCoercions DwithCoercions
  <- elab-complete DwithCoercions Elab
  <- elab-type-soundness Elab Dtarget.

%worlds () (summary-static  _  _ _).
%total  {} (summary-static  _  _ _).



% summary-dynamic: If . |- e : A elaborates to M 
%                  and M evaluates to a value W (in zero or more steps)
%                  then there exists v such that:
%                    e steps to v in zero or more steps
%                    and . |- v : A.

summary-dynamic :
   % If
         {E : exp}
         elab E A M
      -> steptm* M W
      -> is-valuetm W
   % then there exists a value V
      -> {V : exp}
         is-value V
   % such that E steps to V,
      -> step* E V
   % preserving types.
      -> typeof V A
    -> type.
%mode summary-dynamic +E +ElabE +Step*MW +IsValtmW
                      -V -IsVal -Step*EV -TypeofV.

- :
     summary-dynamic E ElabE Step*MW IsValtmW V IsVal Step*EV TypeofV
  <- consistency* ElabE IsValtmW Step*MW Step*EV IsVal ElabV
  <- typeof-erase TypeofV ElabV.

%worlds () (summary-dynamic  _ _ _ _   _ _ _ _).
%total  {} (summary-dynamic  _ _ _ _   _ _ _ _).