fact: Definition entailment_as_conjunctive_statement (e: EqEntailment): Statement := Impl (fold_right Conj (Ext True) (map identity_as_eq (entailment_premises _ e))) (identity_as_eq (entailment_conclusion _ e)).
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.misc.util MathClasses.theory.jections MathClasses.interfaces.ua_basic