proposition: Lemma hash_R_inv x y : #_R x = #_R y -> x = y.
proof: Proof. revert y; induction x; intros [] H; inv H; firstorder congruence. Qed.
imports: Bool List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions