proposition: Lemma included_list_sound : (forall a1 a2 a3, eqA a1 a2 -> eqA a2 a3 -> eqA a1 a3) -> forall l1 l2, (included_list l1 l2 = true) -> forall x, mem x l1 -> mem x l2.
proof: Proof. intro eq_trans. fix included_list_sound 1. intros l1 l2;case l1. intros _ x abs;elim abs. simpl. intros a l H x H0. case H0. revert H; generalize (mem_bool_ok a l2); case (mem_bool a l2). intros a_mem_l2 Heq; rewrite mem_in_eq in a_mem_l2; case a_mem_l2; clear a_mem_l2. intros a' [a_eq_a' a'_in_l2] x_eq_a. rewrite mem_in_eq; exists a'; split; [apply eq_trans with a | idtac]; assumption. intros; discriminate. apply included_list_sound. case (andb_prop _ _ H );auto. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)