proposition: Lemma in_insert : forall (A : Type) (l1 l2 : list A) e a, In a (l1 ++ l2) -> In a (l1 ++ e :: l2).
proof: Proof. intros A l1 l2 e a a_in_l1_l2; destruct (in_app_or _ _ _ a_in_l1_l2) as [a_in_l1 | a_in_l2]; apply in_or_app; [left | right; right]; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)