proposition: Lemma defined_app : forall f l1 l2, defined f (l1 ++ l2) = defined f l1 || defined f l2.
proof: Proof. intros. induction l1; auto. simpl. destruct (lhs a); auto. rewrite IHl1, orb_assoc; refl. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil VecUtil EqUtil BoolUtil) Coq(Sumbool)