proposition: Lemma progress P : (forall Q, ~ step P Q) \/ exists Q, step P Q.
proof: Proof. induction P. - firstorder inv_step. - destruct IHP1 as [H1 | [Q1 H1]]; eauto. destruct IHP2 as [H2 | [Q2 H2]]; eauto. destruct P1. 3:eauto. all: firstorder inv_step. - destruct IHP as [H1 | [Q1 H1]]; eauto. firstorder inv_step. - destruct IHP as [H1 | [Q1 H1]]; eauto. destruct P. 5:eauto. all: firstorder inv_step. - destruct IHP as [H1 | [Q1 H1]]; eauto. firstorder inv_step. 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