proposition: Lemma preservation_star P Q Γ s : typing Γ P s -> Relation_Operators.clos_refl_trans term step P Q -> typing Γ Q s.
proof: Proof. intros H. induction 1; eauto using preservation. 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