proposition: Lemma ΓPCP_soundness_ind {v w P A} : incl A ((v, w) :: P) -> hsc ΓPCP (PCPf ((v, w) :: P) (v ++ (tau1 A)) (w ++ (tau2 A))) -> hsc ΓPCP (PCPf ((v, w) :: P) v w).
proof: Proof. elim /rev_ind : A. { move=> _ /=. by rewrite ? app_nil_r. } move=> [x y] A IH /incl_app_inv [/IH] + /incl_cons_inv [? _]. rewrite tau1_lastP tau2_lastP ? app_assoc. move=> + ?; apply. apply: ΓPCP_step; first by eassumption. apply: ΓPCP_assoc_x. apply: ΓPCP_assoc_y. by assumption. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP