proposition: Theorem foldBody_option_spec : forall (A B : Set)(C D: Type)(eqda : EqDec A)(eqdb : EqDec B) (c1 : A -> C -> Comp (option A)) (c2 : B -> D -> Comp (option B)) (post : A -> B -> Prop) (pre1 : A -> B -> Prop) (pre2 : C -> D -> Prop), (forall a b c d, pre1 a b -> pre2 c d -> comp_spec (opt_pred post) (c1 a c) (c2 b d)) -> forall opt_a opt_b c d, opt_pred pre1 opt_a opt_b -> pre2 c d -> comp_spec (opt_pred post) (foldBody_option _ c1 opt_a c) (foldBody_option _ c2 opt_b d).
proof: Proof. intuition. unfold foldBody_option. unfold opt_pred in *. destruct opt_a; destruct opt_b; intuition. eapply comp_spec_ret; intuition. Qed.
imports: FCF.FCF