proposition: Lemma not_ΓPCP_rrr n r : not (der ΓPCP n (arr r (arr r r))).
proof: Proof. elim: n r; first by move=> ? /derE. move=> n IH r /derE => [[ζ [s [k [+ [+]]]]]]. rewrite /ΓPCP /In -/ΓPCP. case; last case; last case; last case; last case; last done. all: move=> <-. { case: k => [|k] /=; last by move=> /Forall_cons_iff [/IH]. move=> _ [<- _] /(f_equal size) => /=. by lia. } all: case: k => [|k] /=. 1,3,5,7: by (move=> _; case=> _ <-; move /(f_equal size) => /=; by lia). all: case: k => [|k] /=. 1,3,5,7: by (move=> _; case=> <- _; move /(f_equal size) => /=; by lia). all: by move=> /Forall_cons_iff [_] /Forall_cons_iff [/IH]. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP