proposition: Lemma In_Γ_all_skip_lr bound n i : nth_error (Γ_all bound i) (bound + n) = nth_error (Γ_init ++ Γ_step) n.
proof: Proof. rewrite /Γ_all /Γ_lr [nth_error _ (bound + n)]nth_error_app2 map_length seq_length. { lia. } congr nth_error. lia. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun