-| pred_abst: ∀A,C. pred A C → pred (𝛌.A) (𝛌.C)
-| pred_appl: ∀B,D,A,C. pred B D → pred A C → pred (@B.A) (@D.C)
-| pred_beta: ∀B,D,A,C. pred B D → pred A C → pred (@B.𝛌.A) ([⬐D]C)
+| pred_abst: ∀A1,A2. pred A1 A2 → pred (𝛌.A1) (𝛌.A2)
+| pred_appl: ∀B1,B2,A1,A2. pred B1 B2 → pred A1 A2 → pred (@B1.A1) (@B2.A2)
+| pred_beta: ∀B1,B2,A1,A2. pred B1 B2 → pred A1 A2 → pred (@B1.𝛌.A1) ([⬐B2]A2)