proposition: Theorem arrayLookup_f_equiv : forall (A B C : Set) (eqdb : EqDec B) (x1 : list (B * C)) (x2 : list (A * B * C)) (a : B), list_pred (fun c0 d => fst c0 = snd (fst d) /\ snd c0 = snd d) x1 x2 -> arrayLookup _ x1 a = arrayLookup_f _ x2 a.
proof: Proof. induction x1; inversion 1; intuition; simpl in *. subst. destruct a. destruct a2. simpl in *. subst. destruct p. simpl. destruct (eqb a0 b0 ); intuition. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv