proposition: Lemma hsc_der {Gamma t} : hsc Gamma t -> exists n, der Gamma n t.
proof: Proof. elim. - move=> ζ s /der_var => /(_ ζ (substitute ζ s) 0 0). move=> H. exists 1. apply: H; by [|constructor]. - move=> s' t' _ [[|n1] /derE]; [done|]. move=> + _ [[|n2] /derE]; [done|]. move=> [ζ1 [s1 [k1 [Hs1 [? Hk1]]]]]. move=> [ζ2 [s2 [k2 [? [? ?]]]]]. exists (S (S (n1+n2))). apply: (der_var _ (ζ := ζ1) (s := s1) (k := S k1)). + done. + rewrite (arguments_S Hk1). apply /Forall_app. constructor. * apply: Forall_impl; last eassumption. move=> ? /der_mon. apply. by lia. * constructor; last done. apply: der_var; last eassumption; first done. apply: Forall_impl; last eassumption. move=> ? /der_mon. apply. by lia. + apply: target_S. by eassumption. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC