proposition: Theorem Weak A B phi : A ⊢ phi -> A <<= B -> B ⊢ phi.
proof: Proof. intros H. revert B. induction H; intros B HB; try unshelve (solve [econstructor; auto with datatypes]); try now econstructor. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts