-(* the abstract candidate of reducibility associated to an atomic arity *)
-let rec aacr (RP:relation3 genv lenv term) (A:aarity) (G:genv) (L:lenv) on A: predicate term ≝
-λT. match A with
-[ AAtom ⇒ RP G L T
-| APair B A ⇒ ∀L0,V0,T0,des.
- aacr RP B G L0 V0 → ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] T ≡ T0 →
- aacr RP A G L0 (ⓐV0.T0)
+(* the functional construction for candidates *)
+definition cfun: candidate → candidate → candidate ≝
+ λC1,C2,G,K,T. ∀L,V,U,des.
+ ⇩*[Ⓕ, des] L ≡ K → ⇧*[des] T ≡ U → C1 G L V → C2 G L (ⓐV.U).
+
+(* the candidate associated to an atomic arity *)
+let rec aacr (RP:candidate) (A:aarity) on A: candidate ≝
+match A with
+[ AAtom ⇒ RP
+| APair B A ⇒ cfun (aacr RP B) (aacr RP A)