proposition: Lemma doll_hash_L x: x <<= Sigma -> ~ $ el #_L x.
proof: Proof. induction x; intros. -- firstorder. -- intros [ | []]. ++ now eapply fresh_spec in H0 as []. ++ symmetry in H0. eapply fresh_spec in H0 as []. firstorder. ++ firstorder. Qed.
imports: Bool List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions