proposition: Lemma hash_L_diff x y : #_L x <> # :: #_R y.
proof: Proof. revert y. induction x; cbn -[fresh]; intros ? ?; inv H. destruct y; inv H1. firstorder. Qed.
imports: Bool List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions