proposition: Lemma hold_eNOT : forall k e, hold k (eNOT k e) <-> not (hold k e).
proof: Proof. intros k; destruct k ; simpl. - intros. apply iff_refl. - intros e. unfold is_true. rewrite negb_true_iff. destruct e ; intuition congruence. Qed.
imports: List Refl Bool Relation_Definitions Setoid