proposition: Lemma itau_tau2 P A : A <<= P -> itau2 P (f P A) = tau2 A.
proof: Proof. intros H. induction A as [ | (x,y) ]. - reflexivity. - cbn. assert ((x, y) el P) as [n E] % (el_pos card_eq) by firstorder. rewrite E. cbn. unfold f in IHA. rewrite IHA; eauto. now erewrite pos_nth; eauto. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions