proposition: Lemma cnf_checker_sound : forall t w, cnf_checker t w = true -> forall env, eval_cnf env t.
proof: Proof. unfold eval_cnf. intros t; induction t as [|a t IHt]. - simpl. auto. - simpl. intros w; destruct w as [|w ?]. + intros ; discriminate. + case_eq (checker a w) ; intros H H0 env ** ; try discriminate. generalize (@checker_sound _ _ H env). generalize (IHt _ H0 env) ; intros H1 H2. destruct t. * red ; intro. rewrite <- make_conj_impl in H2. tauto. * rewrite <- make_conj_impl in H2. tauto. Qed.
imports: List Refl Bool Relation_Definitions Setoid