proposition: Lemma permut_closure : forall (A : Type) eqA (eqA_dec : forall a1 a2, {eqA a1 a2}+{~eqA a1 a2}), forall a1 a2, @permutation A eqA eqA_dec (a1 :: nil) (a2 :: nil) <-> (forall a, eqA a1 a <-> eqA a2 a).
proof: Proof. intros A eqA eqA_dec; unfold permutation, meq; simpl. intros a1 a2; split. intros H a; assert (Ha := H a); clear H; do 2 rewrite <- plus_n_O in Ha. destruct (eqA_dec a1 a) as [a1_eq_a | a1_diff_a]; destruct (eqA_dec a2 a) as [a2_eq_a | a2_diff_a]. intuition. discriminate. discriminate. intuition. intros H a; destruct (eqA_dec a1 a) as [a1_eq_a | a1_diff_a]; destruct (eqA_dec a2 a) as [a2_eq_a | a2_diff_a]; trivial. absurd (eqA a2 a); trivial; rewrite <- (H a); trivial. absurd (eqA a1 a); trivial; rewrite (H a); trivial. Qed.
imports: Coq(List Relations Multiset Arith Setoid) CoLoR(decidable_set more_list equiv_list)