proposition: Theorem compLoop_spec : forall (A B : Set){e1 : EqDec A}{e2 : EqDec B}(P : A -> B -> Prop)(c1 : A -> Comp A)(c2 : B -> Comp B) n a b, (forall x y, P x y -> comp_spec P (c1 x) (c2 y)) -> P a b -> comp_spec P (compLoop e1 c1 n a) (compLoop e2 c2 n b).
proof: Proof. induction n; intuition. unfold compLoop. simpl. eapply comp_spec_ret; intuition. unfold compLoop in *. simpl. Admitted. Theorem compLoop_eq : forall (A : Set){e1 e2 : EqDec A}(c1 c2 : A -> Comp A) n a x, (forall x y, evalDist (c1 x) y == evalDist (c2 x) y) -> evalDist (compLoop e1 c1 n a) x == evalDist (compLoop e2 c2 n a) x. intuition. eapply (@comp_spec_eq_impl_eq _ e1 e2). eapply compLoop_spec; intuition. subst. eapply eq_impl_comp_spec_eq. eapply H. Qed.
imports: FCF CompFold