proposition: Lemma typing_c_subst : forall (E F : env) e u S T (z : atom), typing_c (F ++ (z ~ S) ++ E) e T -> typing_c E u S -> typing_c (F ++ E) ([z ~> u] e) T.
proof: Proof. Admitted. Lemma typing_c_subst_simple : forall (E : env) e u S T (z : atom), typing_c ((z ~ S) ++ E) e T -> typing_c E u S -> typing_c E ([z ~> u] e) T. Proof. Admitted. Inductive value_c : exp -> Prop := | value_abs_c : forall e T1, lc_c (abs T1 e) -> value_c (abs T1 e). Inductive eval_c : exp -> exp -> Prop := | eval_beta_c : forall e1 e2 T1, lc_c (abs T1 e1) -> value_c e2 -> eval_c (app (abs T1 e1) e2) (open e1 e2) | eval_app_1_c : forall e1 e1' e2, lc_c e2 -> eval_c e1 e1' -> eval_c (app e1 e2) (app e1' e2) | eval_app_2_c : forall e1 e2 e2', value_c e1 -> eval_c e2 e2' -> eval_c (app e1 e2) (app e1 e2'). #[export] Hint Constructors value_c eval_c : core. Lemma preservation_c : forall (E : env) e e' T, typing_c E e T -> eval_c e e' -> typing_c E e' T. Proof. intros E e e' T H. generalize dependent e'. induction H; intros e' J. Admitted. Lemma progress_c : forall e T, typing_c nil e T -> value_c e \/ exists e', eval_c e e'. Proof. intros e T H. assert (typing_c nil e T); auto. remember (@nil (atom * typ)) as E. induction H; subst. Admitted. Lemma typing_c_uniq : forall E e T, typing_c E e T -> uniq E. Proof. intros E e T H. induction H; auto. Case "typing_abs_c". pick fresh x. assert (uniq ((x ~ T1) ++ E)); auto. inversion H1. auto. Qed.
imports: Metalib.Metatheory String