proposition: Theorem _paco6_acc: forall l r (OBG: forall rr (INC: r <6== rr) (CIH: l <6== rr), l <6== paco6 gf rr), l <6== paco6 gf r.
proof: Proof. intros. apply uncurry_adjoint1_6. eapply _paco_acc. intros. apply uncurry_adjoint1_6 in INC. apply uncurry_adjoint1_6 in CIH. apply uncurry_adjoint2_6. eapply le6_trans. eapply (OBG _ INC CIH). apply curry_map6. apply _paco_mon; try apply le1_refl; apply curry_bij1_6. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)