proposition: Lemma overweight_Instruction {M} : weight M <> 0 -> { op | In op M /\ weight_Instruction op <> 0 }.
proof: Proof. elim: M; first done. move=> op M IH /=. have [-> ? |] : { weight M = 0 } + { weight M <> 0 } by decide equality. - exists op. constructor; [by left | done]. - move /IH => [op' [? ?]] _. exists op'. constructor; [by right | done]. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun