proposition: Fact subcode_cons_invert_right j J Q i I : (i,I::nil) <sc (j,J::Q) -> i = j /\ I = J \/ (i,I::nil) <sc (S j,Q).
proof: Proof. intros ([ | K l ] & r & H1 & H2); simpl in *. + inversion H1; left; split; auto; lia. + right; inversion H1; exists l, r; split; auto; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils)