proposition: Lemma xcnf_impl : forall (k: kind) (f1 : GFormula k) (o : option unit) (f2 : GFormula 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 (IMPL f1 o f2)) -> hold k (eval_f e_rtyp (eval env) (if pol then IMPL f1 o f2 else NOT (IMPL f1 o f2))).
proof: Proof. simpl; intros k f1 o f2 IHf1 IHf2 pol env H. unfold mk_impl in H. destruct pol. + simpl. rewrite hold_eIMPL. intro. rewrite or_cnf_opt_correct in H. rewrite or_cnf_correct in H. destruct H as [H | H]. * generalize (IHf1 _ _ H). simpl in *. rewrite hold_eNOT. tauto. * generalize (IHf2 _ _ H). auto. + rewrite eval_cnf_and_opt in H. unfold and_cnf in H. simpl in H. rewrite eval_cnf_app in H. destruct H as [H0 H1]. generalize (IHf1 _ _ H0). generalize (IHf2 _ _ H1). simpl. rewrite ! hold_eNOT. rewrite ! hold_eIMPL. tauto. Qed.
imports: List Refl Bool Relation_Definitions Setoid