proposition: Lemma In_Γ_allE bound i x s phi t : nth_error (Γ_all bound i) x = Some (s, phi) -> In t (s::phi) -> Γ_all_spec bound i x t.
proof: Proof. have [|] : x < length (Γ_lr bound i) \/ x >= length (Γ_lr bound i) by lia. { rewrite /Γ_lr map_length seq_length => Hx. have H'x : forall i', nth_error (Γ_all bound i') x = Some (s_pos i' x). { move=> i'. rewrite /Γ_all nth_error_app1. { by rewrite /Γ_lr map_length seq_length. } by rewrite /Γ_lr nth_error_map nth_error_seq. } rewrite H'x /s_pos. case Eix: (Nat.eqb i x) => /=. { move=> [<- <-]. case; last done. move=> ?. move=> /Nat.eqb_eq in Eix. subst. by apply: Γ_all_lr_l. } case E'ix: (Nat.eqb i (S x)). { move=> [<- <-]. case; last done. move=> ?. move=> /Nat.eqb_eq in E'ix. subst. by apply: Γ_all_lr_r. } move=> [<- <-]. case; last done. move=> <-. move=> /Nat.eqb_neq in Eix. move=> /Nat.eqb_neq in E'ix. by apply: Γ_all_lr_bullet. } rewrite /Γ_all. move=> /[dup] /nth_error_app2 + /nth_Γ_common. rewrite /Γ_all. move=> ->. move: (x - _). case. { move=> /= ? [<- <-]. by do 1 (case; [move=> <-; by eauto using Γ_all_spec, erefl with nocore|]). } case. { move=> /= ? [<- <-]. by do 3 (case; [move=> <-; by eauto using Γ_all_spec, erefl with nocore|]). } case. { move=> /= ? [<- <-]. by do 3 (case; [move=> <-; by eauto using Γ_all_spec, erefl with nocore|]). } case. { move=> /= ? [<- <-]. by do 1 (case; [move=> <-; by eauto using Γ_all_spec, erefl with nocore|]). } move=> x' /=. rewrite /Γ_step nth_error_map. move E: (nth_error rs x') => [[[? ?][? ?]]|]; last done. move=> /(@nth_error_In rule) in E. move=> ? [<- <-] /=. do 2 (case; [move=> <-; by eauto using Γ_all_spec, erefl with nocore|]). move=> /in_map_iff [?] [<-]. by eauto using Γ_all_spec, erefl with nocore. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun