proposition: Lemma ksoundnessT (T : form -> Prop) phi : T ⊢TI phi -> kvalid_theo T phi.
proof: Proof. intros [A[H1 H2 % ksoundness]]. firstorder. Qed.
imports: Undecidability(FOL.Semantics.Kripke.FragmentCore FOL.Deduction.FragmentND) Undecidability(Shared.ListAutomation)