proposition: Lemma soundness_ind {v w P x y A} : incl A ((v, w) :: P) -> x ++ tau1 A = y ++ tau2 A -> hsc (Γ v w P) (encode_pair (encode_word x) (encode_word y)).
proof: Proof. elim: A x y. { move=> x y _ /=. rewrite ? app_nil_r => <-. pose ζ i := if i is 1 then encode_word x else var i. have -> : encode_pair (encode_word x) (encode_word x) = substitute ζ (encode_pair (var 1) (var 1)) by done. apply: hsc_var. rewrite /Γ /In. by left. } move=> [a b] A IH x y /incl_cons_inv [? HA]. rewrite /tau1 -/tau1 /tau2 -/tau2 ? app_assoc. move /IH => /(_ HA) ?. apply: hsc_arr; last eassumption. rewrite ? encode_word_app. pose ζ i := if i is 2 then encode_word x else if i is 3 then encode_word y else var i. have -> : encode_word x = substitute ζ (var 2) by done. have -> : encode_word y = substitute ζ (var 3) by done. rewrite - ? transparent_append_word; try done. rewrite - ? transparent_encode_pair; try done. rewrite - substitute_arrP. apply: hsc_var. rewrite /Γ. right. right. rewrite in_map_iff. exists (a, b). by constructor. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP