(clen c0) t t0 (lift (S O) (clen c0) x))) H4 (lift (S O) (clen c0) x) H7) in
(subst0_gen_lift_false x t (lift (S O) (clen c0) x) (S O) (clen c0) (clen c0)
(le_n (clen c0)) (eq_ind_r nat (plus (S O) (clen c0)) (\lambda (n: nat).(lt
(clen c0) t t0 (lift (S O) (clen c0) x))) H4 (lift (S O) (clen c0) x) H7) in
(subst0_gen_lift_false x t (lift (S O) (clen c0) x) (S O) (clen c0) (clen c0)
(le_n (clen c0)) (eq_ind_r nat (plus (S O) (clen c0)) (\lambda (n: nat).(lt