fact: Record Entailment (P: Type): Type := { entailment_premises: list P; entailment_conclusion: P }.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.misc.util MathClasses.theory.jections MathClasses.interfaces.ua_basic