proposition: Lemma end_is_var_typed Gamma A C: S = Enc C -> (repeat (alpha → alpha) (|S|) ++ Gamma ⊢(3) s : A) -> exists i e, i < |S| /\ s = var i e.
proof: Proof. Proof using x u_neq_v t sigma N H1 EQ. intros H2 H4; destruct end_head_var as (h' & T & s' & H5); intuition idtac; subst. destruct T as [| t1 [| t2 T]]. + cbn in EQ. erewrite nth_error_sapp in EQ; (eauto 2). rewrite nth_error_map_option in H0; destruct nth; try discriminate. cbn in H0; injection H0 as <-. unfold enc in EQ; Discriminate. + exists h'. exists t1. intuition. now eapply nth_error_Some_lt in H0. + eapply AppR_ordertyping_inv in H4. destruct H4 as [L]; intuition. inv H3. rewrite nth_error_app1, nth_error_repeated in H5; simplify in *. inv H2. inv H8. cbn in H5; injection H5 as ?. rewrite !Arr_app in H; cbn in H. eapply (f_equal arity) in H. rewrite arity_Arr in H; cbn in H. lia. all: eapply nth_error_Some_lt in H0; simplify in H0; (eauto 2). Qed.
imports: RelationClasses Morphisms List Lia Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus third_order.pcp)