%%% Simply Typed Lambda Calculus w/ small-step, allocation semantics
%%% Author: Matthew Fluet (June 2005)
%%% loc-lemmas.thm

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Loc Less-than Lemmas
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%theorem
loc!lt_trans_thm :
          forall* {L1:loc} {L2:loc} {L3:loc}
          forall {DLocLt12: loc_lt L1 L2}
                 {DLocLt23: loc_lt L2 L3}
          exists {DLocLt13: loc_lt L1 L3}
          true.
%prove 3 {} (loc!lt_trans_thm _ _ _).

%theorem
loc!lt_contradict_thm :
          forall* {L:loc}
          forall {DLocLt: loc_lt L L}
          exists {Absurd: absurd}
          true.
%prove 2 {} (loc!lt_contradict_thm _ _).