proposition: Fact subcode_cons_inj i ρ δ P : (i,ρ::nil) <sc P -> (i,δ::nil) <sc P -> ρ = δ.
proof: Proof. destruct P as (j, P). intros (l1 & r1 & H1 & H2) (l2 & r2 & H3 & H4). rewrite H1 in H3. apply list_app_inj, proj2 in H3; try lia. inversion H3; trivial. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils)