proposition: Lemma solution_from_PA2_model (M : Model) e : M ⊨ PA2 -> M ⊨ encode_problem e -> H10p e.
proof: Proof. intros M_correct H. eapply H10p_to_PA2_standard_model_sat, PA2_models_agree_FO with (rho := empty_PA2_env _). apply encoding_first_order. apply encoding_closed. apply M_correct. apply H. apply std_model_correct. Qed.
imports: PeanoNat Lia Vector List Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts PA2_categoricity) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.H10(H10p) Undecidability.Shared.Dec