proposition: Lemma is_bool_abst_simpl : forall b (f:TFormula TX AF b), is_bool (abst_simpl f) = is_bool f.
proof: Proof. intros b f; induction f ; simpl ; auto. rewrite needA_all. reflexivity. Qed.
imports: List Refl Bool Relation_Definitions Setoid