proposition: Lemma end_head_var: exists (h: nat) T s', s = AppR (var h) T /\ nth S h = Some s'.
proof: Proof. Proof using x v u_neq_v t sigma N H1 EQ. eapply normal_nf in N as N'. inv N'. destruct k; cbn in *; (auto 5); [|Discriminate]. destruct (s0); cbn in H; intuition idtac; clear H. - assert(f < |S| \/ f >= |S|) as [] by lia; auto. eapply nth_error_lt_Some in H as H2; destruct H2. now eauto. asimpl in EQ; rewrite sapp_ge_in in EQ; (eauto 2). specialize (H1 (f - |S|)). intuition. eapply equiv_head_equal in EQ; cbn; simplify; (eauto 3). simplify in EQ; cbn in EQ; (eauto 1). destruct (sigma (f - (|S|))); cbn in *; intuition. - asimpl in EQ. eapply equiv_head_equal in EQ; cbn; simplify in *; [|auto..]. cbn in EQ; discriminate. Qed.
imports: RelationClasses Morphisms List Lia Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus third_order.pcp)