intros 1; elim i using wf_nat_ind names 0; clear i; intros; split; intros;
[ lapply linear p_inv_O to H; decompose
| lapply linear t_inv_O to H; decompose
| inversion H1; clear H1; intros;
intros 1; elim i using wf_nat_ind names 0; clear i; intros; split; intros;
[ lapply linear p_inv_O to H; decompose
| lapply linear t_inv_O to H; decompose
| inversion H1; clear H1; intros;