proposition: Lemma gpaco2_accF : forall {T0 : Type} {T1 : forall a : T0, Type} (gf : rel2 T0 T1 -> rel2 T0 T1), monotone2 gf -> forall (clo : rel2 T0 T1 -> rel2 T0 T1) (r rg : rel2 T0 T1) (X : Type) (f0 : X -> T0) (f1 : forall x : X, T1 (f0 x)) (OBG : forall rr : rel2 T0 T1, (forall x y, rg x y -> rr x y) -> (forall x, rr (f0 x) (f1 x)) -> forall x : X, gpaco2 gf clo r rr (f0 x) (f1 x)), forall x : X, gpaco2 gf clo r rg (f0 x) (f1 x).
proof: Proof. intros. apply gpaco2_cofix with (l := fun a0 (a1 : T1 a0) => exists x, existT _ (f0 x) (f1 x) = existT _ a0 a1); [ eauto | | eauto ]. intros. change (gpaco2 gf clo r rr (projT1 (existT _ _ x1)) (projT2 (existT _ _ x1))). destruct PR as [? <-]. eauto. Qed.
imports: Paco(paco)