proposition: Lemma step_subst_inv P Q σ τ : step (subst_term σ (τ >> var) P) Q -> exists P', step P P' /\ subst_term σ (τ >> var) P' = Q.
proof: Proof. Proof with eexists; split; [eauto | now_asimpl]. intros H. dependent induction H; rename x into Eqn. - destruct P; inv Eqn. destruct P1; inv H0... - destruct P; inv Eqn. destruct P; inv H0... - destruct P; inv Eqn. destruct (IHstep _ _ _ eq_refl) as (P1' & H1 & <-)... - destruct P; inv Eqn. destruct (IHstep _ _ _ eq_refl) as (P1' & H1 & <-)... - destruct P; inv Eqn. destruct (IHstep _ _ _ eq_refl) as (P1' & H1 & <-)... - destruct P; inv Eqn. edestruct (IHstep P (up_term_poly_type σ) (0 .: τ >> shift)) as (P1' & H1 & <-). now_asimpl. exists (abs p P1'). split. eauto. now_asimpl. - destruct P; inv Eqn. destruct (IHstep _ _ _ eq_refl) as (P1' & H1 & <-)... 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 Coq.Program.Equality