proposition: Lemma In_s_id_rulesI c a b a' b' : In c symbols -> In (arr' [bullet] (arr' [symbol c] (symbol c))) (arr' [isl] (arr' [symbol a'] (symbol a)) :: arr' [isr] (arr' [symbol b'] (symbol b)) :: s_id_rules).
proof: Proof. move=> ?. do 2 right. apply /in_map_iff. by exists c. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun