fact: Definition eval_stmt (vars: Vars A nat): Statement → Prop := fix F (s: Statement) := match s with | Eq _ i => eval vars (fst i) = eval vars (snd i) | Impl a b => F a → F b | Ext P => P | Conj a b => F a ∧ F b | Disj a b => F a ∨ F b end.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.misc.util MathClasses.theory.jections MathClasses.interfaces.ua_basic