proposition: Lemma tau_itau1 P A : (forall a : nat, a el A -> a < | P |) -> tau1 (g P A) = itau1 P A.
proof: Proof. intros H. induction A. - reflexivity. - cbn. unfold g in *. rewrite IHA; firstorder. now destruct (nth a P ([], [])) eqn:E. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions