proposition: Lemma list_forall_option_is_complete_true : forall (A : Type) f l, (forall a, In a l -> f a = Some true) -> @list_forall_option A f l = Some true.
proof: Proof. intros A f l; induction l as [ | a l]. simpl; intros; trivial. intro H; simpl; rewrite (H _ (or_introl _ (eq_refl _))); apply IHl; intros; apply H; right; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)