proposition: Lemma end_is_var: (forall x, x ∈ S -> isVar x) -> exists i e, i < |S| /\ s = var i e.
proof: Proof. Proof using x t sigma N H1 EQ. intros H2; edestruct @end_head_var with (X:=X) as (h' & T & s' & H5 & ?); (eauto 2). subst s. destruct T as [| t1 [| t2 T]]. all: cbn in EQ; specialize (H1 h'). all: destruct (sigma h') eqn: H'; cbn in *; intuition idtac. 1, 3: eapply nth_error_In in H as H7; eapply H2 in H7. 1, 2: eapply nth_error_sapp in H; rewrite ?H in EQ. + destruct s'; cbn in *; intuition idtac. Discriminate. + rewrite AppR_subst in EQ; cbn in EQ. eapply equiv_app_elim in EQ as (EQ1 & EQ2); cbn; trivial; simplify. destruct s'; cbn in *; intuition idtac. rewrite H in EQ1. 2: rewrite H; (auto 3). exfalso. symmetry in EQ1. eapply equiv_neq_var_app; (eauto 1); simplify; (eauto 3). + exists h'. exists t1. intuition idtac. eauto using nth_error_Some_lt. Unshelve. exact 0. Qed.
imports: RelationClasses Morphisms List Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus unification.unification) Undecidability.HOU(third_order.pcp third_order.encoding)