proposition: Lemma F_term rho1 rho2 t : rho1 ≈ rho2 -> F (eval rho1 t) (eval rho2 t).
proof: Proof. Proof using M2_correct M1_correct. revert t. apply (term_ind (fun t => rho1 ≈ rho2 -> F (eval rho1 t) (eval rho2 t))); intros. - apply H. - apply H, Forall2_Forall. induction v. easy. split. now apply IH. apply IHv, IH. - destruct f; cbn in v; revert IH. + pattern v. apply Vector.case0. intros. exact F_O. + apply (Vector.caseS' v). intros ? v0. pattern v0. apply Vector.case0. intros IH. apply F_S. now apply IH. + apply (Vector.caseS' v). intros ? v1. apply (Vector.caseS' v1). intros ? v0. pattern v0. apply Vector.case0. intros IH. apply F_add; now apply IH. + apply (Vector.caseS' v). intros ? v1. apply (Vector.caseS' v1). intros ? v0. pattern v0. apply Vector.case0. intros IH. apply F_mul; now apply IH. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts)