proposition: Lemma Γ_lr_bound_S bound : Γ_lr bound (S bound) = map (fun=> (bullet, [])) (seq 0 bound).
proof: Proof. apply: map_ext_in => j /in_seq ?. rewrite /s_pos. have /Nat.eqb_neq -> : S bound <> j by lia. by have /Nat.eqb_neq -> : S bound <> S j by 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