proposition: Lemma tauto_checker_sound : forall t w, tauto_checker t w = true -> forall env, eval_f e_rtyp (eval env) t.
proof: Proof. unfold tauto_checker. intros t w H env. change (eval_f e_rtyp (eval env) t) with (eval_f e_rtyp (eval env) (if true then t else TT isProp)). apply (xcnf_correct t true). eapply cnf_checker_sound ; eauto. Qed.
imports: List Refl Bool Relation_Definitions Setoid