DEFINITION arity_gen_cvoid_subst0()
TYPE =
       ∀g:G
         .∀c:C
           .∀t:T
             .∀a:A
               .arity g c t a
                 →∀d:C
                      .∀u:T
                        .∀i:nat
                          .getl i c (CHead d (Bind Void) u)
                            →∀w:T.∀v:T.(subst0 i w t v)→∀P:Prop.P
BODY =
Show proof