proposition: Fact bsm_sss_total ii s : { t | ii // s -1> t }.
proof: Proof. destruct s as (i,v). destruct ii as [ x p q | x b ]. + case_eq (v#>x); [ intros Hx | intros [] l Hx ]. * exists (q,v); constructor; trivial. * exists (1+i,v[l/x]); constructor; trivial. * exists (p,v[l/x]); constructor; trivial. + exists (1+i,v[(b::v#>x)/x]); constructor. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss)