proposition: Lemma R_canonical_functional : functional Canonical_Rel.
proof: Proof. hnf. intros x (y1&z1) (y2&z2) (c1&k1&H1&<-&H1') (c2&k2&H2&<-&H2'). pose proof loop_injective H1 H2 as ->. congruence. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM