\forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (a: A).((arity g
c1 t1 a) \to (\forall (c2: C).((wcpr0 c1 c2) \to (\forall (t2: T).((pr0 t1
t2) \to (arity g c2 t2 a)))))))))
\forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (a: A).((arity g
c1 t1 a) \to (\forall (c2: C).((wcpr0 c1 c2) \to (\forall (t2: T).((pr0 t1
t2) \to (arity g c2 t2 a)))))))))
\forall (t1: T).(\forall (t2: T).((pr1 t1 t2) \to (\forall (g: G).(\forall
(c1: C).(\forall (a: A).((arity g c1 t1 a) \to (\forall (c2: C).((wcpr0 c1
c2) \to (arity g c2 t2 a)))))))))
\forall (t1: T).(\forall (t2: T).((pr1 t1 t2) \to (\forall (g: G).(\forall
(c1: C).(\forall (a: A).((arity g c1 t1 a) \to (\forall (c2: C).((wcpr0 c1
c2) \to (arity g c2 t2 a)))))))))
\forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall
(g: G).(\forall (a: A).((arity g c t1 a) \to (arity g c t2 a)))))))
\def
\forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall
(g: G).(\forall (a: A).((arity g c t1 a) \to (arity g c t2 a)))))))
\def
(arity_sred_wcpr0_pr0 g c0 t3 a H3 c0 (wcpr0_refl c0) t4 H1) d u i H0 t
H2)))))))))))))) c t1 t2 H)))).
(arity_sred_wcpr0_pr0 g c0 t3 a H3 c0 (wcpr0_refl c0) t4 H1) d u i H0 t
H2)))))))))))))) c t1 t2 H)))).
\forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr3 c t1 t2) \to (\forall
(g: G).(\forall (a: A).((arity g c t1 a) \to (arity g c t2 a)))))))
\def
\forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr3 c t1 t2) \to (\forall
(g: G).(\forall (a: A).((arity g c t1 a) \to (arity g c t2 a)))))))
\def