proposition: Lemma not_mem_compat : forall s2 e e', eq_A e e' -> (fun e0 : EDS1.A => negb (mem_bool eq_bool e0 (support s2))) e = (fun e0 : EDS1.A => negb (mem_bool eq_bool e0 (support s2))) e'.
proof: Proof. intros s2 e e' e_eq_e'; generalize (mem_bool_ok _ _ eq_bool_ok e (support s2)) (mem_bool_ok _ _ eq_bool_ok e' (support s2)). case (mem_bool eq_bool e (support s2)); case (mem_bool eq_bool e' (support s2)). intros _ _; reflexivity. intros e_in_s2 e'_not_in_s2; absurd (more_list.mem eq_A e' (support s2)). assumption. apply (mem_eq_mem eq_proof e); assumption. intros e_not_in_s2 e'_in_s2; absurd (more_list.mem eq_A e (support s2)). assumption. apply (mem_eq_mem eq_proof e'). apply (equiv_sym _ _ eq_proof); assumption. assumption. intros _ _; reflexivity. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)