proposition: Lemma xcnf_true_mk_arrow_r : forall b o t (f:TFormula TX AF b), xcnf true (mk_arrow o f (X b t)) = xcnf false f.
proof: Proof. intros b o; destruct o ; simpl; auto. - intros t f. destruct (is_X f) eqn:EQ. + apply is_X_inv in EQ. subst. reflexivity. + simpl. apply or_cnf_opt_cnf_ff_r. - intros. apply or_cnf_opt_cnf_ff_r. Qed.
imports: List Refl Bool Relation_Definitions Setoid