proposition: Theorem compFold_option_spec : forall (A B : Set)(lsa : list A)(lsb : list B)(pre : A -> B -> Prop), list_pred pre lsa lsb -> forall (C D : Set){eqdc : EqDec C}{eqdd : EqDec D}(c1 : C -> A -> Comp (option C))(c2 : D -> B -> Comp (option D))(post : C -> D -> Prop) c d, (forall c d a b, post c d -> pre a b -> comp_spec (opt_pred post) (c1 c a) (c2 d b)) -> opt_pred post c d -> comp_spec (opt_pred post) (compFold _ (foldBody_option _ c1) c lsa) (compFold _ (foldBody_option _ c2) d lsb).
proof: Proof. induction 1; intuition; simpl. eapply comp_spec_ret; intuition. eapply comp_spec_seq; eauto. eapply foldBody_option_spec; eauto. Qed.
imports: FCF.FCF