proposition: Theorem arrayLookup_perm_eq : forall (A B : Set)(eqd : EqDec A)(ls1 ls2 : list (A * B)), Permutation ls1 ls2 -> NoDup (fst (split ls1)) -> NoDup (fst (split ls2)) -> (forall x, arrayLookup _ ls1 x = arrayLookup _ ls2 x).
proof: Proof. induction 1; intuition idtac; simpl in *. destruct x. case_eq (eqb x0 a); intros. trivial. remember (split l') as z. destruct z. remember (split l) as z. destruct z. simpl in *. inversion H0; clear H0; subst. inversion H1; clear H1; subst. eapply IHPermutation; eauto. destruct y. destruct x. remember (split l) as z. destruct z. simpl in *. case_eq (eqb x0 a); intros. rewrite (eqb_leibniz) in H1. subst. case_eq (eqb a a0); intros. rewrite eqb_leibniz in H1. subst. inversion H0; clear H0; subst. simpl in *. intuition idtac. trivial. reflexivity. rewrite H3. rewrite IHPermutation2. trivial. eapply Permutation_NoDup. eapply fst_split_perm; eauto. trivial. trivial. eapply Permutation_NoDup. eapply fst_split_perm; eauto. trivial. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold