proposition: Theorem arrayLookup_pair_snd : forall (A B C : Set)(eqda : EqDec A)(eqdb : EqDec B)(ls1 : list (A * B * C))(ls2 : list (B * C)) a b, list_pred (fun x y => fst (fst x) = a /\ snd (fst x) = fst y /\ snd x = snd y) ls1 ls2 -> arrayLookup _ ls1 (a, b) = arrayLookup _ ls2 b.
proof: Proof. induction ls1; intuition; simpl in *. inversion H; clear H; subst. simpl. trivial. inversion H; clear H; subst. simpl. intuition. subst. simpl in *. subst. destruct a2. simpl in *. unfold eqbPair. simpl. rewrite eqb_refl. simpl. case_eq (eqb b1 b); intuition. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold