proposition: Lemma adequate_step {v w P n} : adequate v w P (S n) -> adequate v w P n \/ solving v w P n.
proof: Proof. move=> [p [q /derE]] => [[ζ [s [k]]]]. rewrite {1}/Γ /In -/(In _ _). case. case; last case. { move=> ?. subst s. case: k. { move=> [_] /=. case=> -> ->. move=> /(f_equal size) /=. by lia. } move=> k /= [/Forall_cons_iff] [? _] _. left. eexists. eexists. by eassumption. } { move=> ?. subst s. case: k. { move=> [_] /=. case=> <- _. case=> _ /(f_equal size) /=. by lia. } move=> k /= [/Forall_cons_iff] [? _] _. right. exists []. constructor; first done. eexists. rewrite ? app_nil_r /=. by eassumption. } { move /in_map_iff => [[x y] [<- _]] /=. case: k; last case. - move=> [_] /=. case=> <- _. case=> _ _ _ /(f_equal size) /=. by lia. - move=> [_] /=. case=> <- _. move=> /(f_equal size) /=. by lia. - move=> k /= [/Forall_cons_iff] [_] /Forall_cons_iff [? _] _. left. eexists. eexists. by eassumption. } Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP