proposition: Lemma paco2_accF : forall {T0 : Type} {T1 : forall a : T0, Type} (gf : rel2 T0 T1 -> rel2 T0 T1) (r : rel2 T0 T1) (X : Type) (f0 : X -> T0) (f1 : forall x : X, T1 (f0 x)), (forall rr : rel2 T0 T1, (forall a0 a1, r a0 a1 -> rr a0 a1) -> (forall x, rr (f0 x) (f1 x)) -> forall x : X, paco2 gf rr (f0 x) (f1 x)) -> forall x : X, paco2 gf r (f0 x) (f1 x).
proof: Proof. intros. apply paco2_acc with (l := fun a0 (a1 : T1 a0) => exists x, existT _ (f0 x) (f1 x) = existT _ a0 a1); [ | eauto ]. intros rr INC CIH x0 x1 PR. change (paco2 gf rr (projT1 (existT _ _ x1)) (projT2 (existT _ _ x1))). destruct PR as [? <-]. eauto. Qed.
imports: Paco(paco)