T).((pr2 c (THead (Bind Void) u (lift (S O) O t)) t2) \to (eq T (THead (Bind
Void) u (lift (S O) O t)) t2))))).(\lambda (P: Prop).(nf2_gen__nf2_gen_aux
Void t u O (H t (pr2_free c (THead (Bind Void) u (lift (S O) O t)) t
T).((pr2 c (THead (Bind Void) u (lift (S O) O t)) t2) \to (eq T (THead (Bind
Void) u (lift (S O) O t)) t2))))).(\lambda (P: Prop).(nf2_gen__nf2_gen_aux
Void t u O (H t (pr2_free c (THead (Bind Void) u (lift (S O) O t)) t