proposition: Lemma mk_iff_is_bool : forall (k: kind) (f1 f2:TFormula TX AF k) pol, match is_bool f2 with | Some isb => xcnf (if isb then pol else negb pol) f1 | None => mk_iff xcnf pol f1 f2 end = mk_iff xcnf pol f1 f2.
proof: Proof. intros k f1 f2 pol. destruct (is_bool f2) as [b|] eqn:EQ; auto. apply is_bool_inv in EQ. subst. unfold mk_iff. destruct b ; simpl; cnf_simpl; reflexivity. Qed.
imports: List Refl Bool Relation_Definitions Setoid