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