proposition: Lemma xcnf_true_mk_arrow_l : forall b o t (f:TFormula TX AF b), xcnf true (mk_arrow o (X b t) f) = xcnf true f.
proof: Proof. intros b o; destruct o ; simpl; auto. intros. rewrite or_cnf_opt_cnf_ff. reflexivity. Qed.
imports: List Refl Bool Relation_Definitions Setoid