proposition: Lemma match_start d' B : d' :: B <<= P -> tau1 (d' :: B) = tau2 (d' :: B) -> d' = d.
proof: Proof. intros Hs Hm. assert (d' el P) as [ -> | [ -> | (x & y & ? & -> & ?) ] ] % P_inv by now eapply Hs; cbn -[fresh] in Hm. - congruence. - inv Hm. now edestruct fresh_spec; eauto. - cbn in Hm. destruct x, y; try firstorder congruence. + destruct (tau1_inv Hm) as (x' & y' & ? ). pose (cons_incl Hs). assert ( (n :: x') / y' el P) as [] % P_inv_top by eauto. eapply sym_word_R; eauto. + cbn -[fresh] in Hm. symmetry in Hm. destruct (tau2_inv Hm) as (x' & y' & ? ). pose (cons_incl Hs). assert ( y' / (# :: x') el P) as [] % P_inv_bot by eauto. + cbn -[fresh] in Hm. inversion Hm. assert (fresh (dollar :: Sigma) = hash) by reflexivity. edestruct fresh_spec; try eassumption. right. eapply sym_word_R in H. subst. eauto. Qed.
imports: Bool List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions