proposition: Lemma Mult_rec x y : Gamma ⊢ ( (σ x) ⊗ y == y ⊕ (x ⊗ y) ).
proof: Proof. Proof using G. apply Weak with FAeq. pose (sigma := [x ; y] ∗ var). change (FAeq ⊢ _) with (FAeq ⊢ ((σ $1) ⊗ $0 == $0 ⊕ ($1 ⊗ $0))[sigma]). eapply subst_forall_prv with 2. apply Ctx. all : firstorder. repeat solve_bounds. Qed.
imports: Undecidability.FOL.Arithmetics(FA Signature) Undecidability.FOL(PA) Lia List Vector