instance LO.Propositional.Hilbert.F.instAczelSlashable {Ax : Axiom ℕ} (hs : ∀ {φ : Formula ℕ}, φ ∈ Ax → ∕ₐ[Hilbert.F Ax] φ) : (Hilbert.F Ax).AczelSlashable

theorem LO.Propositional.slashable_axiomSer {Ax : Axiom ℕ} [Entailment.HasAxiomSer (Hilbert.F Ax)] : ∕ₐ[Hilbert.F Ax] Axioms.Ser

theorem LO.Propositional.slashable_axiomTra1 {Ax : Axiom ℕ} {φ ψ χ : Formula ℕ} [Entailment.HasAxiomTra1 (Hilbert.F Ax)] : ∕ₐ[Hilbert.F Ax] (Axioms.Tra1 φ ψ χ)

theorem LO.Propositional.slashable_axiomRfl {Ax : Axiom ℕ} {φ ψ : Formula ℕ} [Entailment.HasAxiomRfl (Hilbert.F Ax)] : ∕ₐ[Hilbert.F Ax] (Axioms.Rfl φ ψ)

theorem LO.Propositional.slashable_propvar_axiomHrd {Ax : Axiom ℕ} {a : ℕ} (h : ∀ (a : ℕ), Hilbert.F Ax ⊢ #a ➝ ⊤ ➝ #a) : ∕ₐ[Hilbert.F Ax] (Axioms.Hrd #a)

instance LO.Propositional.F.AczelSlashable : Propositional.F.AczelSlashable

instance LO.Propositional.F.Disjunctive : Entailment.Disjunctive Propositional.F

instance LO.Propositional.F_Ser.AczelSlashable : Propositional.F_Ser.AczelSlashable

instance LO.Propositional.F_Ser.Disjunctive : Entailment.Disjunctive Propositional.F_Ser

instance LO.Propositional.F_Rfl.AczelSlashable : Propositional.F_Rfl.AczelSlashable

instance LO.Propositional.F_Rfl.Disjunctive : Entailment.Disjunctive Propositional.F_Rfl

instance LO.Propositional.F_Tra1.AczelSlashable : Propositional.F_Tra1.AczelSlashable

instance LO.Propositional.F_Tra1.Disjunctive : Entailment.Disjunctive Propositional.F_Tra1

instance LO.Propositional.F_Tra1_Hrd.AczelSlashable : Propositional.F_Tra1_Hrd.AczelSlashable

instance LO.Propositional.F_Tra1_Hrd.Disjunctive : Entailment.Disjunctive Propositional.F_Tra1_Hrd

instance LO.Propositional.F_Rfl_Tra1_Hrd.AczelSlashable : Propositional.F_Rfl_Tra1_Hrd.AczelSlashable

instance LO.Propositional.F_Rfl_Tra1_Hrd.Disjunctive : Entailment.Disjunctive Propositional.F_Rfl_Tra1_Hrd