proposition: Lemma target_S {r s t k} : target k r = arr s t -> target (S k) r = t.
proof: Proof. elim: k r s t; first by move=> > /= ->. by move=> k IH [> /= | > /= /IH <-]. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC