proposition: Lemma nil_not_in_r1: ~ ([] \in R1).
proof: Proof. unfold R1; intros N. inversion N; subst; clear N. inversion H2; subst; clear H2. induction s1. { simpl in H4. inversion H4. } inversion H4. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang