proposition: Lemma contains_one_false_strict: forall a, contains_one a = false -> strict a.
proof: Proof. induction a; simpl; intro Ha; try discriminate; auto. destruct (contains_one a1); auto. destruct (contains_one a1); auto. discriminate. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(Monoid) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(Model_RegExp) Coq(Bool)