proposition: Lemma preservation P Q Γ s : typing Γ P s -> step P Q -> typing Γ Q s.
proof: Proof. induction 1 in Q |- *. - inversion 1. - inversion 1; subst. + inversion H; subst. eapply typing_subst_term. eassumption. intros [] ? [=]; subst; cbn; eauto using typing. + eauto using typing. + eauto using typing. - inversion 1; subst. eauto using typing. - inversion 1; subst. + inversion H; subst. evar (Gamma' : environment). replace Gamma with Gamma'. all: subst Gamma'. eapply typing_subst_poly_type. eassumption. erewrite List.map_map, List.map_ext, List.map_id. reflexivity. intros. now asimpl. + eauto using typing. - inversion 1; subst. eauto using typing. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.typing_facts Undecidability.SystemF.Util.term_facts Coq.Relations.Relation_Operators