DEFINITION nf2_gen_void()
TYPE =
       ∀c:C.∀u:T.∀t:T.(nf2 c (THead (Bind Void) u (lift (S O) O t)))→∀P:Prop.P
BODY =
Show proof