proposition: Lemma nth_Γ_common x bound i i' : x >= length (Γ_lr bound i) -> nth_error (Γ_all bound i') x = nth_error (Γ_all bound i) x.
proof: Proof. move=> Hx. rewrite /Γ_all [LHS]nth_error_app2. { move: Hx. by rewrite /Γ_lr !map_length !seq_length. } rewrite [RHS]nth_error_app2; first done. by rewrite /Γ_lr !map_length !seq_length. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun