proposition: Lemma mult_rec : forall n d : D, iσ d i⊗ n = n i⊕ d i⊗ n.
proof: Proof. Proof using ext_model FA_model. intros n d. assert (List.In ax_mult_rec FA) as H by firstorder. specialize (FA_model ax_mult_rec (d.:(fun _ => iO)) H). cbn in FA_model. now apply ext_model. Qed.
imports: Undecidability.FOL.Arithmetics(FA Signature) Undecidability.FOL(PA) Lia List Vector