proposition: Fact pctm_sss_fun ρ s t1 t2 : ρ // s -1> t1 -> ρ // s -1> t2 -> t1 = t2.
proof: Proof. intros []; subst; inversion 1; subst; auto; try mydiscr; myinj. Qed.
imports: List Bool Arith Lia Undecidability.Shared.Libs.DLW(subcode sss) Undecidability.TM(SBTM)