proposition: Theorem randomFunc_hist_spec : forall (ls1 ls2 : list (D * R)), lookupEq _ ls1 ls2 -> forall d, comp_spec (fun p1 p2 => fst p1 = fst p2 /\ lookupEq _ (snd p1) (snd p2)) (randomFunc RndR _ ls1 d) (randomFunc_hist ls2 d).
proof: Proof. intros. unfold randomFunc, randomFunc_hist. rewrite H. case_eq (arrayLookup _ ls2 d); intros. fcf_simp. eapply comp_spec_ret; intuition idtac. unfold lookupEq. intuition idtac. simpl. case_eq (eqb d0 d); intros. rewrite eqb_leibniz in H1. subst. rewrite H. trivial. eauto. fcf_skip. eapply comp_base_exists; eauto. eapply comp_base_exists; eauto. eapply comp_spec_ret; intuition idtac. unfold lookupEq; intuition idtac; simpl. rewrite H. reflexivity. Qed.
imports: FCF.FCF FCF.CompFold FCF.Array FCF.Hybrid