proposition: Fact sss_compute_inv P st1 st2 st3 : out_code (fst st3) P -> P // st1 ->> st2 -> P // st1 ->> st3 -> P // st2 ->> st3.
proof: Proof. Proof using sss_fun. intros H2 (p & H3) (k & H4). apply subcode_sss_subcode_inv with (3 := H3) in H4; auto. destruct H4 as (q & _ & ?); exists q; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)