proposition: Fact bsm_sss_fun i s t1 t2 : i // s -1> t1 -> i // s -1> t2 -> t1 = t2.
proof: Proof. intros []; subst; inversion 1; subst; auto; try mydiscr; myinj. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss)