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