proposition: Lemma is_tauto_is_correct : forall be : bool_expr, is_tauto be = true -> is_valid be.
proof: Proof. unfold is_tauto, is_valid in |- *. intros. elim (BDDof_bool_expr_correct be initBDDconfig initBDDneg_memo initBDDor_memo initBDDconfig_OK initBDDneg_memo_OK_2 initBDDor_memo_OK). intros. elim H1. intros. elim H3. intros. elim H5. intros. elim H7. intros. rewrite <- (Neqb_complete _ _ H) in H9. exact (bool_fun_eq_trans _ _ _ (bool_fun_eq_symm _ _ H9) (bool_fun_of_BDDone _ H0) vb). Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4 bdd5_1 bdd5_2 bdd6 bdd7 BDDdummy_lemma_2 BDDdummy_lemma_3 BDDdummy_lemma_4 bdd8 bdd9 bdd10 bdd11