proposition: Lemma nth_Γ_lr i j bound : j < bound -> nth_error (Γ_all bound i) j = Some (s_pos i j).
proof: Proof. move=> ?. rewrite /Γ_all /Γ_lr nth_error_app1. { by rewrite map_length seq_length. } by rewrite nth_error_map nth_error_seq. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun