proposition: Lemma hash_L_app x y : #_L (x ++ y) = #_L x ++ #_L y.
proof: Proof. induction x; cbn in *; now try rewrite IHx. Qed.
imports: Bool List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions