tp : type. tm : type. % Types arr : tp -> tp -> tp. % Terms app : tm -> tm -> tm. lam : tp -> (tm -> tm) -> tm. % Values value : tm -> type. step: tm -> tm -> type. s_app1 : step E1 E1' -> % -------------------------- step (app E1 E2) (app E1' E2). s_app2 : value E1 -> step E2 E2' -> % -------------------------- step (app E1 E2) (app E1 E2'). s_app3 : value E2 -> % -------------------------- step (app (lam T (\x. E1 x)) E2) (E1 E2). % Typing has_type : tm -> tp -> type. is_app : has_type E1 (arr T1 T2) -> has_type E2 T1 -> % ------------------- has_type (app E1 E2) T2. is_lam : ({x:tm} has_type x T1 -> has_type (E x) T2) -> % ----------------------------------- has_type (lam T1 (\x. E x)) (arr T1 T2). % Preservation rec pres : [ |- has_type E T] -> [ |- step E E'] -> [ |- has_type E' T] = fn d => fn s => case s of [ |- s_app1 S1] => let [ |- is_app D1 D2] = d in let [ |- D1'] = pres [ |- D1] [ |- S1] in [ |- is_app D1' D2] | [ |- s_app2 V S2] => let [ |- is_app D1 D2] = d in let [ |- D2'] = pres [ |- D2] [ |- S2] in [ |- is_app D1 D2'] | [ |- s_app3 V] => let [ |- is_app (is_lam (\x. (\d. (D1 x d)))) D2] = d in [ |- (D1 _ D2)] ;