proposition: Lemma hold_eIFF_IMPL : forall k e1 e2, hold k (eIFF k e1 e2) <-> (hold k (eAND k (eIMPL k e1 e2) (eIMPL k e2 e1))).
proof: Proof. intros. rewrite hold_eIFF. rewrite hold_eAND. rewrite! hold_eIMPL. tauto. Qed.
imports: List Refl Bool Relation_Definitions Setoid