proposition: Lemma P_inv_bot x y : ~(y, # :: x) el P.
proof: Proof. intros [ | [ | (x'' & y' & ? & ? & ?) ] ] % P_inv. - inv H. edestruct fresh_spec; eauto. - inv H. edestruct fresh_spec; eauto. - inv H0. destruct y'; cbn -[fresh] in *; [congruence | ]. inversion H4. edestruct fresh_spec with (l := dollar :: Sigma); [ | reflexivity ]. unfold hash in *. rewrite H2. right. eapply sym_word_R; eauto. Qed.
imports: Bool List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions