proposition: Lemma xcnf_iff : forall (k : kind) (f1 f2 : @GFormula Term rtyp Annot unit k) (IHf1 : forall (pol : bool) (env : Env), eval_cnf env (xcnf pol f1) -> hold k (eval_f e_rtyp (eval env) (if pol then f1 else NOT f1))) (IHf2 : forall (pol : bool) (env : Env), eval_cnf env (xcnf pol f2) -> hold k (eval_f e_rtyp (eval env) (if pol then f2 else NOT f2))), forall (pol : bool) (env : Env), eval_cnf env (xcnf pol (IFF f1 f2)) -> hold k (eval_f e_rtyp (eval env) (if pol then IFF f1 f2 else NOT (IFF f1 f2))).
proof: Proof. simpl. intros k f1 f2 IHf1 IHf2 pol env H. rewrite mk_iff_is_bool in H. unfold mk_iff in H. destruct pol; rewrite or_cnf_opt_correct in H; rewrite or_cnf_correct in H; rewrite! eval_cnf_and_opt in H; unfold and_cnf in H; rewrite! eval_cnf_app in H; generalize (IHf1 false env); generalize (IHf1 true env); generalize (IHf2 false env); generalize (IHf2 true env); simpl. - rewrite hold_eIFF_IMPL. rewrite hold_eAND. rewrite! hold_eIMPL. rewrite! hold_eNOT. tauto. - rewrite! hold_eNOT. rewrite hold_eIFF_IMPL. rewrite hold_eAND. rewrite! hold_eIMPL. tauto. Qed.
imports: List Refl Bool Relation_Definitions Setoid